OAI/Analysis/DirectCrouzeix/AnalyticCharts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectCrouzeix.Geometry.analytic_inverse_chart line 31
  2. def OAI.DirectCrouzeix.Geometry.conjugatePair line 53
  3. theorem OAI.DirectCrouzeix.Geometry.conjugatePair_continuous line 55
  4. theorem OAI.DirectCrouzeix.Geometry.conjugatePair_zero line 58
  5. theorem OAI.DirectCrouzeix.Geometry.normalized_implicit_graph line 60
  6. theorem OAI.DirectCrouzeix.Geometry.negative_vertical_level_side line 130
  7. theorem OAI.DirectCrouzeix.Geometry.analytic_complex_chart line 187
  8. def OAI.DirectCrouzeix.Geometry.expLevel line 237