OAI/Analysis/StrictMeans/DiskAutomorphisms.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.not_eventually_constant_of_injOn line 18
  2. lemma OAI.StrictInverseFirstPower.analytic_injOn_map_nhds line 30
  3. lemma OAI.StrictInverseFirstPower.invFunOn_continuousAt line 37
  4. lemma OAI.StrictInverseFirstPower.deriv_eventually_ne_zero_of_injOn line 49
  5. theorem OAI.StrictInverseFirstPower.deriv_ne_zero_of_injOn line 65
  6. lemma OAI.StrictInverseFirstPower.second_deriv_eq_twice_dslope line 114
  7. lemma OAI.StrictInverseFirstPower.second_deriv_norm_le_four line 140
  8. def OAI.StrictInverseFirstPower.diskAutomorphism line 148
  9. lemma OAI.StrictInverseFirstPower.diskAutomorphism_den_ne line 150
  10. lemma OAI.StrictInverseFirstPower.diskAutomorphism_norm_identity line 160
  11. lemma OAI.StrictInverseFirstPower.diskAutomorphism_mapsTo line 166
  12. lemma OAI.StrictInverseFirstPower.diskAutomorphism_injOn line 179
  13. lemma OAI.StrictInverseFirstPower.diskAutomorphism_hasDerivAt line 192
  14. lemma OAI.StrictInverseFirstPower.diskAutomorphism_differentiableOn line 200
  15. lemma OAI.StrictInverseFirstPower.diskAutomorphism_zero line 205
  16. lemma OAI.StrictInverseFirstPower.diskAutomorphism_deriv_zero line 207
  17. lemma OAI.StrictInverseFirstPower.diskAutomorphism_second_deriv_zero line 211
  18. lemma OAI.StrictInverseFirstPower.second_deriv_comp line 225