OAI/Analysis/Crouzeix/ContourPolynomials.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Contour Polynomials.

  1. theorem OAI.CrouzeixHilbert.SmoothContour.integral_deriv_mul_pow line 21
  2. theorem OAI.CrouzeixHilbert.smul_resolvent_eq line 37
  3. theorem OAI.CrouzeixHilbert.contourEval_mul_id_of_integral_eq_zero line 49
  4. theorem OAI.CrouzeixHilbert.contourEval_pow line 96
  5. theorem OAI.CrouzeixHilbert.contourEval_const_mul line 106
  6. theorem OAI.CrouzeixHilbert.contourEval_sum line 111
  7. theorem OAI.CrouzeixHilbert.contourEval_pow_mul_const line 121
  8. theorem OAI.CrouzeixHilbert.contourEval_matrixPolynomial_entry line 127
  9. theorem OAI.CrouzeixHilbert.matrixContourEval_matrixPolynomial line 139
  10. theorem OAI.CrouzeixHilbert.contourEval_polynomial line 157
  11. theorem OAI.CrouzeixHilbert.contour_bound_of_uniform_polynomials line 168
  12. theorem OAI.CrouzeixHilbert.contourEval_congr line 180
  13. theorem OAI.CrouzeixHilbert.contourEval_mul_sub_of_integral_eq_zero line 190
  14. theorem OAI.CrouzeixHilbert.SmoothContour.integral_deriv_div_eq_zero line 204
  15. theorem OAI.CrouzeixHilbert.contourEval_inv_sub line 212