OAI/Analysis/DirectCrouzeix/DiskMapping.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectCrouzeix.Conformal.diskMobius line 29
  2. theorem OAI.DirectCrouzeix.Conformal.diskMobius_den_ne_zero line 31
  3. theorem OAI.DirectCrouzeix.Conformal.diskMobius_difference line 39
  4. theorem OAI.DirectCrouzeix.Conformal.diskMobius_mapsTo line 46
  5. theorem OAI.DirectCrouzeix.Conformal.diskMobius_hasDerivAt line 57
  6. theorem OAI.DirectCrouzeix.Conformal.diskMobius_deriv_ne_zero line 68
  7. theorem OAI.DirectCrouzeix.Conformal.diskMobius_injOn line 74
  8. theorem OAI.DirectCrouzeix.Conformal.diskMobius_self line 85
  9. theorem OAI.DirectCrouzeix.Conformal.diskMobius_zero line 87
  10. theorem OAI.DirectCrouzeix.Conformal.diskMobius_norm_deriv line 89
  11. theorem OAI.DirectCrouzeix.Conformal.diskMobius_norm_deriv_zero line 97
  12. theorem OAI.DirectCrouzeix.Conformal.diskMobius_norm_deriv_self line 102
  13. theorem OAI.DirectCrouzeix.Conformal.hasDerivAt_squareRoot line 112
  14. theorem OAI.DirectCrouzeix.Conformal.improve_embedding line 130
  15. theorem OAI.DirectCrouzeix.Conformal.exists_riemannMap line 219
  16. theorem OAI.DirectCrouzeix.Conformal.inverse_hasStrictDerivAt line 229
  17. theorem OAI.DirectCrouzeix.Conformal.inverse_holomorphic line 237
  18. theorem OAI.DirectCrouzeix.Conformal.compact_inverse_disk line 243
  19. theorem OAI.DirectCrouzeix.Conformal.norm_tendsto_one_boundary line 257