OAI/Analysis/Crouzeix/PolynomialApproximation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Polynomial Approximation.

  1. theorem OAI.CrouzeixHilbert.SmoothContour.integral_deriv_mul_eq_zero_of_holomorphic line 19
  2. theorem OAI.CrouzeixHilbert.SmoothContour.cauchy_formula_convex line 40
  3. def OAI.CrouzeixHilbert.compactCauchyKernel line 70
  4. theorem OAI.CrouzeixHilbert.continuous_compactCauchyKernel line 78
  5. theorem OAI.CrouzeixHilbert.compactCauchyKernel_mem_iff_resolvent line 87
  6. theorem OAI.CrouzeixHilbert.coordinate_resolventSet_subset_compl line 112
  7. theorem OAI.CrouzeixHilbert.compactCauchyKernel_mem_polynomialClosure line 122
  8. def OAI.CrouzeixHilbert.compactCauchyKernelExtension line 156
  9. theorem OAI.CrouzeixHilbert.compactCauchyKernelExtension_apply line 161
  10. theorem OAI.CrouzeixHilbert.continuousOn_compactCauchyKernelExtension line 169
  11. theorem OAI.CrouzeixHilbert.intervalIntegral_mem_closedSubalgebra line 176
  12. theorem OAI.CrouzeixHilbert.holomorphic_mem_polynomialClosure_of_convex_neighborhood line 187
  13. theorem OAI.CrouzeixHilbert.exists_polynomial_uniform_approx line 235
  14. theorem OAI.CrouzeixHilbert.matrix_norm_le_entry_bound line 266
  15. theorem OAI.CrouzeixHilbert.exists_matrixPolynomial_entries line 285
  16. theorem OAI.CrouzeixHilbert.exists_matrixPolynomial_uniform_approx line 304
  17. theorem OAI.CrouzeixHilbert.exists_matrixPolynomial_tendstoUniformlyOn line 323
  18. theorem OAI.CrouzeixHilbert.exists_contour_bound_of_polynomial_bound line 341
  19. theorem OAI.CrouzeixHilbert.holomorphicEval_eq_contourEval_of_independent line 363
  20. theorem OAI.CrouzeixHilbert.nonzeroConclusion_of_finite_bound_and_contour_independence line 372