OAI/Analysis/NumericalRange/DiskMapping.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompleteCrouzeix.diskAut line 28
  2. lemma OAI.CompleteCrouzeix.diskAut_den_ne line 30
  3. lemma OAI.CompleteCrouzeix.diskAut_normSq_identity line 37
  4. lemma OAI.CompleteCrouzeix.diskAut_maps line 45
  5. lemma OAI.CompleteCrouzeix.diskAut_inj line 55
  6. lemma OAI.CompleteCrouzeix.diskAut_deriv line 66
  7. lemma OAI.CompleteCrouzeix.diskAut_zero line 75
  8. lemma OAI.CompleteCrouzeix.diskAut_self line 76
  9. lemma OAI.CompleteCrouzeix.diskAut_deriv_zero_norm line 78
  10. lemma OAI.CompleteCrouzeix.diskAut_deriv_self_norm line 90
  11. lemma OAI.CompleteCrouzeix.holomorphic_square_root line 101
  12. lemma OAI.CompleteCrouzeix.square_root_improvement line 120
  13. theorem OAI.CompleteCrouzeix.bounded_riemann_mapping line 194
  14. theorem OAI.CompleteCrouzeix.partialHomeomorph_analytic_inverse line 211
  15. theorem OAI.CompleteCrouzeix.partialHomeomorph_deriv_ne_zero line 241
  16. theorem OAI.CompleteCrouzeix.holomorphic_injective_inverse line 255
  17. lemma OAI.CompleteCrouzeix.analytic_local_inverse_neighborhood line 293
  18. lemma OAI.CompleteCrouzeix.conformal_extension_boundary_norm line 311
  19. theorem OAI.CompleteCrouzeix.conformal_inverse_boundary_limit line 324
  20. theorem OAI.CompleteCrouzeix.conformal_extension_injOn_closure line 362