OAI/Analysis/StrictMeans/MorseGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StrictInverseFirstPower.realHessian_eq_second line 11
2. lemma OAI.StrictInverseFirstPower.squaredReciprocalPotential_eq_sq line 18
3. lemma OAI.StrictInverseFirstPower.squaredReciprocalPotential_sublevel line 24
4. lemma OAI.StrictInverseFirstPower.squaredReciprocalPotential_lt_sublevel line 36
5. lemma OAI.StrictInverseFirstPower.squaredReciprocalPotential_fderiv_off_pole line 44
6. lemma OAI.StrictInverseFirstPower.squaredReciprocalPotential_critical_iff line 59
7. lemma OAI.StrictInverseFirstPower.squaredReciprocalPotential_hessian_det line 69
8. lemma OAI.StrictInverseFirstPower.squaredReciprocalPotential_hessian_det_pole line 94