OAI/Analysis/Crouzeix/DiskBoundaryChart.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Disk Boundary Chart.

  1. def OAI.CrouzeixHilbert.Conformal.localCayley line 16
  2. theorem OAI.CrouzeixHilbert.Conformal.localCayley_zero line 18
  3. theorem OAI.CrouzeixHilbert.Conformal.localCayley_injOn line 20
  4. theorem OAI.CrouzeixHilbert.Conformal.localCayley_norm_lt_one line 26
  5. theorem OAI.CrouzeixHilbert.Conformal.localCayley_norm_le_one line 34
  6. theorem OAI.CrouzeixHilbert.Conformal.analyticAt_localCayley line 42
  7. theorem OAI.CrouzeixHilbert.Conformal.analyticOnNhd_symm line 46
  8. theorem OAI.CrouzeixHilbert.Conformal.closure_image_subdisk line 54
  9. theorem OAI.CrouzeixHilbert.Conformal.boundaryChart_image_subdisk line 65