OAI/Analysis/Crouzeix/ContourExistence.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Contour Existence.

  1. theorem OAI.CrouzeixHilbert.sub_div_sub_mem_slitPlane line 16
  2. theorem OAI.CrouzeixHilbert.SmoothContour.intervalIntegrable_indexIntegrand line 44
  3. theorem OAI.CrouzeixHilbert.SmoothContour.index_eq_of_segment_avoids line 55
  4. theorem OAI.CrouzeixHilbert.SmoothContour.index_eq_zero_of_re_pos line 87
  5. theorem OAI.CrouzeixHilbert.SmoothContour.index_eq_zero_of_convex line 108
  6. theorem OAI.CrouzeixHilbert.exists_smooth_radial_frontier_approx line 128
  7. def OAI.CrouzeixHilbert.unitCirclePath line 159
  8. theorem OAI.CrouzeixHilbert.unitCirclePath_norm line 161
  9. theorem OAI.CrouzeixHilbert.unitCirclePath_ne_zero line 164
  10. theorem OAI.CrouzeixHilbert.unitCirclePath_smooth line 169
  11. theorem OAI.CrouzeixHilbert.unitCirclePath_closed line 172
  12. theorem OAI.CrouzeixHilbert.hasDerivAt_unitCirclePath line 176
  13. def OAI.CrouzeixHilbert.radialContour line 183
  14. theorem OAI.CrouzeixHilbert.radialContour_index_center line 188
  15. theorem OAI.CrouzeixHilbert.exists_calculusContour line 226