OAI/Analysis/Crouzeix/Convexity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Convexity of the numerical range and its closure.

  1. theorem OAI.CrouzeixHilbert.phase_real line 20
  2. theorem OAI.CrouzeixHilbert.unit_interval_of_quadratic_endpoints line 36
  3. theorem OAI.CrouzeixHilbert.convex_numericalRange line 101
  4. theorem OAI.CrouzeixHilbert.convex_numericalClosure line 130
  5. theorem OAI.CrouzeixHilbert.hilbert_geometry line 133