OAI/Geometry/Relativity/CKS/CKSLogData.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CKSMixedGeometry.SourceMassFields line 12
2. def OAI.CKSMixedGeometry.SourceMassFields.logFields line 22
3. lemma OAI.CKSMixedGeometry.angularProjection_logRadiusChart line 33
4. structure OAI.CKSMixedGeometry.SourceMassFields.RegularAt line 38
5. lemma OAI.CKSMixedGeometry.source_logFields_regular line 48
6. lemma OAI.CKSMixedGeometry.source_logGammaRadial_actual line 60
7. def OAI.CKSMixedGeometry.sourceGamma line 70
8. def OAI.CKSMixedGeometry.sourceTangentialK line 73
9. def OAI.CKSMixedGeometry.sourceRadialMetric line 76
10. lemma OAI.CKSMixedGeometry.sourceGamma_pullback line 79
11. lemma OAI.CKSMixedGeometry.sourceTangentialK_pullback line 85
12. lemma OAI.CKSMixedGeometry.sourceRadialMetric_pullback line 91
13. structure OAI.CKSMixedGeometry.SourceMassFields.ComponentBounds line 97
14. lemma OAI.CKSMixedGeometry.source_log_remainder_bounds line 103