OAI/Geometry/Relativity/CKS/MetricComparisonAssembly.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSAngularGeometry.comparisonFactor line 12
2. lemma OAI.CKSAngularGeometry.comparisonFactor_nonneg line 14
3. lemma OAI.CKSAngularGeometry.comparisonFactor_le_one line 21
4. lemma OAI.CKSAngularGeometry.comparisonFactor_tendsto line 30
5. lemma OAI.CKSAngularGeometry.uniform_error line 49
6. lemma OAI.CKSAngularGeometry.metric_comparison_uniform line 52
7. lemma OAI.CKSAngularGeometry.quadratic3_radialNormalize line 71
8. lemma OAI.CKSAngularGeometry.radialScale_ne_zero line 78
9. lemma OAI.CKSAngularGeometry.radialNormalize_comparison line 87