OAI/Analysis/Crouzeix/Sharpness.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A two-dimensional operator with sharp constant two.

  1. def OAI.CrouzeixHilbert.sharpOperator line 20
  2. def OAI.CrouzeixHilbert.sharpCoefficients line 24
  3. theorem OAI.CrouzeixHilbert.norm_sharpOperator line 26
  4. theorem OAI.CrouzeixHilbert.sharpOperator_apply line 30
  5. theorem OAI.CrouzeixHilbert.sharpOperator_inner_norm line 35
  6. theorem OAI.CrouzeixHilbert.sharpOperator_numerical_le line 42
  7. theorem OAI.CrouzeixHilbert.sharpOperator_numerical_attains line 50
  8. theorem OAI.CrouzeixHilbert.sharp_matrixPolynomial line 70
  9. theorem OAI.CrouzeixHilbert.sharp_polynomialEval line 75
  10. theorem OAI.CrouzeixHilbert.sharpConstant line 79