OAI/Analysis/Crouzeix/Riemann.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Riemann.

  1. structure OAI.CrouzeixHilbert.Conformal.DiskEmbedding line 15
  2. theorem OAI.CrouzeixHilbert.Conformal.derivative_values_bddAbove line 21
  3. theorem OAI.CrouzeixHilbert.Conformal.exists_extremal line 29
  4. theorem OAI.CrouzeixHilbert.Conformal.exists_holomorphic_square_root line 79
  5. theorem OAI.CrouzeixHilbert.Conformal.exists_improved_of_omitted line 101
  6. theorem OAI.CrouzeixHilbert.Conformal.exists_diskEmbedding_of_bounded line 166
  7. theorem OAI.CrouzeixHilbert.Conformal.riemann_mapping_bounded line 184