OAI/Analysis/Crouzeix/RationalContours.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Rational Contours.

  1. theorem OAI.CrouzeixHilbert.SmoothContour.integral_deriv_mul_inv_pow_succ_succ line 20
  2. theorem OAI.CrouzeixHilbert.SmoothContour.integral_deriv_mul_inv_pow line 53
  3. theorem OAI.CrouzeixHilbert.SmoothContour.integral_deriv_mul_polynomial line 61
  4. theorem OAI.CrouzeixHilbert.denominator_eq_prod line 73
  5. theorem OAI.CrouzeixHilbert.polynomial_quotient_partialFractions line 80
  6. theorem OAI.CrouzeixHilbert.SmoothContour.integral_deriv_mul_quotient line 135
  7. theorem OAI.CrouzeixHilbert.contourEval_pow_mul_of_integral_eq_zero line 193
  8. theorem OAI.CrouzeixHilbert.contourEval_polynomial_mul_of_integral_eq_zero line 207
  9. theorem OAI.CrouzeixHilbert.CalculusContour.inside_subset line 225
  10. theorem OAI.CrouzeixHilbert.contourEval_quotient line 230
  11. theorem OAI.CrouzeixHilbert.contourEval_rational line 267
  12. theorem OAI.CrouzeixHilbert.matrixContourEval_matrixRationalFunction line 275
  13. theorem OAI.CrouzeixHilbert.holomorphicEval_rational line 286
  14. theorem OAI.CrouzeixHilbert.matrixHolomorphicEval_matrixRationalFunction line 294
  15. theorem OAI.CrouzeixHilbert.rational_poleFree_neighborhood line 305
  16. theorem OAI.CrouzeixHilbert.rational_conclusion_of_holomorphic_bound line 326