OAI/Geometry/Relativity/CKS/AngularWeighted.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSAngularGeometry.rescale line 12
2. lemma OAI.CKSAngularGeometry.inverse_rescale line 15
3. lemma OAI.CKSAngularGeometry.christoffel_rescale line 23
4. lemma OAI.CKSAngularGeometry.inverseDerivative_rescale line 33
5. lemma OAI.CKSAngularGeometry.christoffelDerivative_rescale line 46
6. lemma OAI.CKSAngularGeometry.ricci_rescale line 56
7. lemma OAI.CKSAngularGeometry.scalar_rescale line 60
8. lemma OAI.CKSAngularGeometry.lapse_rescale line 69
9. theorem OAI.CKSAngularGeometry.weighted_curvature_lapse line 78