OAI/Geometry/Relativity/CKS/LocalMaximumHessian.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSSchwarzschild.localMax_second_deriv_nonpos line 11
2. lemma OAI.CKSSchwarzschild.affineLine_hasDerivAt line 23
3. lemma OAI.CKSSchwarzschild.line_deriv line 27
4. lemma OAI.CKSSchwarzschild.line_second_deriv line 33
5. lemma OAI.CKSSchwarzschild.curve_normSq_second line 51
6. lemma OAI.CKSSchwarzschild.maximum_radius_hessian line 68