OAI/Analysis/NumericalRange/ConformalGluing.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CompleteCrouzeix.analytic_open_gluing line 26
  2. theorem OAI.CompleteCrouzeix.noncritical_holomorphic_inverse line 49
  3. theorem OAI.CompleteCrouzeix.conformal_chart_extension line 88
  4. theorem OAI.CompleteCrouzeix.analytic_family_gluing line 158
  5. lemma OAI.CompleteCrouzeix.analytic_boundary_lens_agreement line 177
  6. theorem OAI.CompleteCrouzeix.analytic_boundary_patch line 213
  7. lemma OAI.CompleteCrouzeix.bounded_holomorphic_local_deriv line 280
  8. lemma OAI.CompleteCrouzeix.bounded_holomorphic_local_lipschitz line 294
  9. theorem OAI.CompleteCrouzeix.bounded_holomorphic_equicontinuous line 306
  10. theorem OAI.CompleteCrouzeix.bounded_holomorphic_subsequence line 332
  11. theorem OAI.CompleteCrouzeix.zero_free_locally_uniform_limit line 377
  12. theorem OAI.CompleteCrouzeix.injOn_locally_uniform_limit line 434
  13. def OAI.CompleteCrouzeix.NormalizedUnivalent line 462
  14. lemma OAI.CompleteCrouzeix.exists_normalized_univalent line 465
  15. theorem OAI.CompleteCrouzeix.exists_extremal_univalent line 485