Polynomial approximation of continuous exterior Cauchy integrals

This file turns the exterior-kernel Runge theorem into an integral theorem. A continuous family of kernels is integrated in the Banach space of continuous functions on the compact set. Closed-convex-hull approximation gives finite sampled kernel sums, and a diagonal choice of their polynomial approximants converges uniformly to the full integral.

theorem exists_cauchyKernel_finset_tendstoUniformlyOn_setIntegral (K : Set ℂ) (hK : IsCompact K) (coeff pole : ℝ → ℂ) (hcoeff : Continuous coeff) (hpole_cont : Continuous pole) (hpole : ∀ (t : ℝ), pole t ∉ K) {a b : ℝ} (hab : a < b) : ∃ (s : ℕ → Finset ↑(Set.Ioc a b)) (w : ℕ → ↑(Set.Ioc a b) → ℝ), TendstoUniformlyOn (fun (n : ℕ) (z : ℂ) => ∑ t ∈ s n, ↑(w n t) * coeff ↑t * (pole ↑t - z)⁻¹) (fun (z : ℂ) => ∫ (t : ℝ) in Set.Ioc a b, coeff t * (pole t - z)⁻¹) Filter.atTop K

A continuous exterior-kernel integral is the compact-uniform limit of finite kernel sums sampled from its parameter interval.

theorem exists_polynomial_tendstoUniformlyOn_intervalIntegral_mul_inv_sub_of_isCompact_convex (K : Set ℂ) (hK : IsCompact K) (hconvex : Convex ℝ K) (coeff pole : ℝ → ℂ) (hcoeff : Continuous coeff) (hpole_cont : Continuous pole) (hpole : ∀ (t : ℝ), pole t ∉ K) {a b : ℝ} (hab : a < b) : ∃ (q : ℕ → Polynomial ℂ), TendstoUniformlyOn (fun (n : ℕ) (z : ℂ) => Polynomial.eval z (q n)) (fun (z : ℂ) => ∫ (t : ℝ) in a..b, coeff t * (pole t - z)⁻¹) Filter.atTop K

A continuous interval integral of Cauchy kernels whose poles stay outside a compact convex planar set is a compact-uniform limit of polynomials.