OAI/Geometry/Relativity/CKS/CollarNullNormalization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSAngularGeometry.lapseResidual_factor line 12
2. def OAI.CKSAngularGeometry.physicalNullQuadratic line 19
3. def OAI.CKSAngularGeometry.physicalNullEta line 29
4. lemma OAI.CKSAngularGeometry.radius_ratios line 34
5. lemma OAI.CKSAngularGeometry.quadratic_rescale line 39
6. lemma OAI.CKSAngularGeometry.physicalNullQuadratic_factor line 51
7. lemma OAI.CKSAngularGeometry.physicalNullEta_factor line 55
8. def OAI.CKSAngularGeometry.coordinateSmallNull line 64
9. lemma OAI.CKSAngularGeometry.null_mass_algebra line 73
10. lemma OAI.CKSAngularGeometry.coordinateSmallNull_factor_z line 81
11. theorem OAI.CKSAngularGeometry.coordinateSmallNull_factor line 101