OAI/Analysis/HilbertCrouzeix/Sharpness.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HilbertCrouzeix.sharpOperator line 16
  2. def OAI.HilbertCrouzeix.sharpPolynomial line 20
  3. theorem OAI.HilbertCrouzeix.sharpPolynomial_apply line 22
  4. theorem OAI.HilbertCrouzeix.sharpPolynomial_norm line 25
  5. theorem OAI.HilbertCrouzeix.sharpOperator_apply line 28
  6. theorem OAI.HilbertCrouzeix.sharpOperator_numerical_le_one line 33
  7. theorem OAI.HilbertCrouzeix.sharpPolynomial_sup_le_one line 45
  8. theorem OAI.HilbertCrouzeix.sharpPolynomial_sup_nonneg line 54
  9. theorem OAI.HilbertCrouzeix.sharpPolynomialEval_norm_ge_two line 67
  10. theorem OAI.HilbertCrouzeix.uniformlySharp line 87