OAI/Analysis/DirectCrouzeix/PolynomialCalculus.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectCrouzeix.exteriorCorrection line 13
  2. def OAI.DirectCrouzeix.exteriorKernel line 16
  3. theorem OAI.DirectCrouzeix.re_circle_fraction line 19
  4. theorem OAI.DirectCrouzeix.exteriorKernel_nonneg_off_diagonal line 34
  5. def OAI.DirectCrouzeix.coefficientEmbedding line 47
  6. def OAI.DirectCrouzeix.tensorPolynomial line 58
  7. def OAI.DirectCrouzeix.coefficientPolynomial line 68
  8. theorem OAI.DirectCrouzeix.kronecker_pow_one line 73
  9. theorem OAI.DirectCrouzeix.tensorPolynomial_C line 81
  10. theorem OAI.DirectCrouzeix.tensorPolynomial_X line 86
  11. theorem OAI.DirectCrouzeix.tensorPolynomial_coefficientPolynomial line 90
  12. theorem OAI.DirectCrouzeix.tensorPolynomial_mul line 98