(*Set up some basic definitions*)

Delta[r_,M_,a_]:=r^2-2*M*r+a^2;
Sigma[r_,a_,theta_]:=r^2+a^2*Cos[theta]^2;

denom=r^(3/4) (r^(3/2)-3 M r^(1/2)+2 a M^(1/2))^(1/2);
En=(r^(3/2)-2 M r^(1/2)+a M^(1/2))/denom;
l=M^(1/2) (r^2-2 a M^(1/2) r^(1/2)+a^2)/denom;

metric={-1,1,1,1};
xxx={t,r,theta,phi};

(*Matrix of elements to convert from unhatted to hatted basis*)
basismatrix[r_,M_,a_,theta_]:=Simplify[{ {(r^2+a^2)/Sqrt[Sigma[r,a,theta]*Delta[r,M,a]],0,0,a/Sqrt[Sigma[r,a,theta]*Delta[r,M,a]]},{0,Sqrt[Delta[r,M,a]/Sigma[r,a,theta]],0,0},{0,0,1/Sqrt[Sigma[r,a,theta]],0},{-a*Sin[theta]/Sqrt[Sigma[r,a,theta]],0,0,-1/Sin[theta]/Sqrt[Sigma[r,a,theta]]}},Sin[theta]≠0]
Simplify[MatrixForm[basismatrix[r,M,a,theta]]]

(*Matrix of elements to convert from hatted to unhatted basis*)
inversebasis=Simplify[{ {Sqrt[Delta[r,M,a]/Sigma[r,a,theta]],0,0,-a*Sin[theta]^2*Sqrt[Delta[r,M,a]/Sigma[r,a,theta]]},{0,1/Sqrt[Delta[r,M,a]/Sigma[r,a,theta]],0,0},{0,0,Sqrt[Sigma[r,a,theta]],0},{a*Sin[theta]/Sqrt[Sigma[r,a,theta]],0,0,-(r^2+a^2)*Sin[theta]/Sqrt[Sigma[r,a,theta]]}},Sin[theta]≠0];
MatrixForm[Simplify[inversebasis/.a^2+2r^2+a^2 Cos[2 theta]->2*Sigma[r,a,theta],r^2+a^2*Cos[theta]^2>0]]

(*Connection coefficients in the unhatted basis*)
Concoeff[l_,m_,n_]:=Simplify[Sum[basismatrix[r,M,a,theta][[l,k]]*D[basismatrix[r,M,a,theta][[m,n]],xxx[[k]]]-basismatrix[r,M,a,theta][[m,k]]*D[basismatrix[r,M,a,theta][[l,n]],xxx[[k]]],{k,4}],r>0&&r^2+a^2Cos[theta]^2>0]
(*Connection coefficients in the hatted basis*)
Coeff[l_,m_,n_]:=Sum[Concoeff[l,m,k]*inversebasis[[k,n]],{k,4}]*metric[[n]]
(*Compute lambda in the hatted basis*)
Lambda[alpha_,beta_,gamma_]:=Simplify[1/2*metric[[alpha]]*(Coeff[alpha,beta,gamma]+Coeff[alpha,gamma,beta]-Coeff[beta,gamma,alpha]),r>0&&a>0&&M>0]

(*the u-vector*)
uvector:={(Energy*(r^2+a^2)-a*L)/(r*Sqrt[Delta[r,M,a]]),0,0,(a*Energy-L)/r}

(*Try to show orthonormality of lambda-bar vectors*)

KK=(a*Energy-L)^2;

(*Coeffs in front of the hatted basis vectors in lambda*)
AA=(Energy(r^2+a^2)-a*L)/Sqrt[Delta[r,M,a]*(r^2+KK)];
B0=Sqrt[KK]*(Energy(r^2+a^2)-a*L)/r/Sqrt[Delta[r,M,a]*(r^2+KK)];
B3=(Sqrt[r^2+KK]/r)*((Energy*a-L)/Sqrt[KK]);

(*Compute the relavant quantities*)
uDotu=Simplify[-uvector[[1]]^2+uvector[[4]]^2/.Energy->En/.L->l,r>0&&M>0&&a>0]
Asquared=Simplify[AA^2/.Energy->En/.L->l,r>0&&M>0&&a>0]
Bsquared=Simplify[(-B0^2+B3^2)/.Energy->En/.L->l,r>0&&M>0&&a>0]
UDotB=Simplify[(-uvector[[1]]*B0+uvector[[4]]*B3)/.Energy->En/.L->l,r>0&&M>0&&a>0&&r>a&&M>a&&((a^2)+r (-2 M+r))>0]