OAI/Analysis/StrictMeans/GenericTargets.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StrictInverseFirstPower.real_complex_log_norm_fderiv line 118
2. lemma OAI.StrictInverseFirstPower.logPotential_branch_contDiffAt line 135
3. lemma OAI.StrictInverseFirstPower.critical_branch_derivative line 144
4. lemma OAI.StrictInverseFirstPower.critical_branch_difference_nz line 176
5. lemma OAI.StrictInverseFirstPower.singular_values_null line 217
6. lemma OAI.StrictInverseFirstPower.criticalMap_contDiffOn line 227
7. lemma OAI.StrictInverseFirstPower.logPotential_eq_log_criticalHeight line 232
8. lemma OAI.StrictInverseFirstPower.critical_inverse_chart_data line 244
9. lemma OAI.StrictInverseFirstPower.critical_inverse_branch_contDiffOn line 258
10. lemma OAI.StrictInverseFirstPower.inverse_chart_pair_ties_null line 269
11. theorem OAI.StrictInverseFirstPower.ae_regular_distinct_critical_heights line 311
12. theorem OAI.StrictInverseFirstPower.affine_law_ae_good_pairs line 368