OAI/Geometry/Relativity/CKS/SchwarzschildCompleteness.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSSchwarzschild.velocity_abs_bound line 13
2. lemma OAI.CKSSchwarzschild.lapseSquared_bound line 23
3. def OAI.CKSSchwarzschild.logRadius line 33
4. lemma OAI.CKSSchwarzschild.logRadius_smooth line 34
5. lemma OAI.CKSSchwarzschild.mfderiv_logRadius line 39
6. lemma OAI.CKSSchwarzschild.logRadius_derivative_bound line 52
7. lemma OAI.CKSSchwarzschild.logRadius_sublevel_compact line 67
8. theorem OAI.CKSSchwarzschild.source_complete line 77