Closure of convex Runge kernel approximations

Finite Cauchy-kernel quadrature approximations naturally produce a sequence of functions, each of which is itself a compact-uniform polynomial limit. This file diagonalizes those iterated limits. Combined with finite exterior Cauchy-kernel approximation, it turns uniform approximation by quadrature sums into uniform approximation by one polynomial sequence.

theorem exists_polynomial_tendstoUniformlyOn_of_iterated_limits (K : Set ℂ) (f : ℂ → ℂ) (g : ℕ → ℂ → ℂ) (hg : TendstoUniformlyOn g f Filter.atTop K) (hpoly : ∀ (n : ℕ), ∃ (q : ℕ → Polynomial ℂ), TendstoUniformlyOn (fun (j : ℕ) (z : ℂ) => Polynomial.eval z (q j)) (g n) Filter.atTop K) : ∃ (q : ℕ → Polynomial ℂ), TendstoUniformlyOn (fun (n : ℕ) (z : ℂ) => Polynomial.eval z (q n)) f Filter.atTop K

A uniform limit of uniform polynomial limits admits one polynomial approximating sequence.

theorem exists_polynomial_tendstoUniformlyOn_of_tendstoUniformlyOn_cauchyKernel_finset (K : Set ℂ) (hK : IsCompact K) (hconvex : Convex ℝ K) (poles : ℕ → Finset ℂ) (coeff : ℕ → ℂ → ℂ) (hpoles : ∀ (n : ℕ), ∀ ζ ∈ poles n, ζ ∉ K) {f : ℂ → ℂ} (hlim : TendstoUniformlyOn (fun (n : ℕ) (z : ℂ) => ∑ ζ ∈ poles n, coeff n ζ * (ζ - z)⁻¹) f Filter.atTop K) : ∃ (q : ℕ → Polynomial ℂ), TendstoUniformlyOn (fun (n : ℕ) (z : ℂ) => Polynomial.eval z (q n)) f Filter.atTop K

A compact-uniform limit of finite exterior Cauchy-kernel sums on a compact convex planar set is itself a compact-uniform limit of polynomials.