OAI/Geometry/Relativity/CKS/BoundaryBridge.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSMain.coefficientAtlas_exists line 24
2. def OAI.CKSMain.schwarzschildAtlas line 30
3. def OAI.CKSMain.horizonNormal line 81
4. lemma OAI.CKSMain.horizon_radius line 84
5. lemma OAI.CKSMain.horizonNormal_coordinate line 87
6. def OAI.CKSMain.schwarzschildBoundary line 106
7. lemma OAI.CKSMain.constant_radius_hessian line 139
8. lemma OAI.CKSMain.constant_radius_second_form line 153
9. lemma OAI.CKSMain.constant_radius_mean line 175
10. lemma OAI.CKSMain.schwarzschildMarginal line 186