OAI/Geometry/Relativity/CKS/SchwarzschildConnection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSSchwarzschild.radialUnit_inner_self line 11
2. lemma OAI.CKSSchwarzschild.tangentProjection_orthogonal line 13
3. lemma OAI.CKSSchwarzschild.cartMetric_tangent line 16
4. lemma OAI.CKSSchwarzschild.cartTensor_tangent line 18
5. lemma OAI.CKSSchwarzschild.radial_connection_tangent line 22
6. lemma OAI.CKSSchwarzschild.tangentProjection_normSq line 47
7. lemma OAI.CKSSchwarzschild.sphereMeanCurvature_eq line 53
8. lemma OAI.CKSSchwarzschild.sphereTensorTrace_eq line 73
9. theorem OAI.CKSSchwarzschild.horizon_expansion line 91