OAI/Geometry/Relativity/CKS/CollarNullRatio.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSAngularGeometry.ratioResidual line 11
2. lemma OAI.CKSAngularGeometry.ratioResidual_smooth line 14
3. lemma OAI.CKSAngularGeometry.nullRatio_factor line 21
4. lemma OAI.CKSAngularGeometry.inverse_hyperbolic_ratio line 29
5. lemma OAI.CKSAngularGeometry.inverse_hyperbolic_ratio_bound line 36
6. lemma OAI.CKSAngularGeometry.nullRatio_bound line 43
7. lemma OAI.CKSAngularGeometry.nullRatio_difference line 59