OAI/Analysis/StrictMeans/CriticalPotential.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StrictInverseFirstPower.logPotential line 104
2. lemma OAI.StrictInverseFirstPower.complex_log_norm_fderiv line 107
3. lemma OAI.StrictInverseFirstPower.logPotential_differentiableAt line 130
4. lemma OAI.StrictInverseFirstPower.logPotential_fderiv_apply line 136
5. lemma OAI.StrictInverseFirstPower.logPotential_critical_iff line 156
6. def OAI.StrictInverseFirstPower.criticalHeight line 212
7. lemma OAI.StrictInverseFirstPower.criticalMap_ne_image line 215
8. lemma OAI.StrictInverseFirstPower.criticalMap_sub_image line 225
9. lemma OAI.StrictInverseFirstPower.criticalHeight_pos line 231
10. lemma OAI.StrictInverseFirstPower.criticalHeight_value line 236
11. lemma OAI.StrictInverseFirstPower.criticalHeight_superlevel line 246
12. lemma OAI.StrictInverseFirstPower.continuous_criticalMap line 260
13. lemma OAI.StrictInverseFirstPower.continuous_criticalHeight line 266
14. lemma OAI.StrictInverseFirstPower.criticalMap_contDiffAt line 274
15. lemma OAI.StrictInverseFirstPower.jacobianExpression_zero_iff line 282