OAI/Analysis/NumericalRange/Sharpness.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompleteCrouzeix.sharpMatrix line 12
  2. def OAI.CompleteCrouzeix.sharpPolynomial line 14
  3. lemma OAI.CompleteCrouzeix.sharpPolynomial_value line 16
  4. lemma OAI.CompleteCrouzeix.sharpPolynomial_value_norm line 19
  5. lemma OAI.CompleteCrouzeix.sharpMatrix_apply line 22
  6. lemma OAI.CompleteCrouzeix.sharpMatrix_pairing line 29
  7. lemma OAI.CompleteCrouzeix.sharpMatrix_numericalRange_le line 35
  8. lemma OAI.CompleteCrouzeix.one_mem_sharpMatrix_numericalRange line 44
  9. lemma OAI.CompleteCrouzeix.sharp_rangeMaximum line 62
  10. lemma OAI.CompleteCrouzeix.sharpPolynomial_at line 76
  11. lemma OAI.CompleteCrouzeix.sharp_tensor_apply line 80
  12. lemma OAI.CompleteCrouzeix.two_le_sharpPolynomial_norm line 93
  13. theorem OAI.CompleteCrouzeix.optimal_constant line 100