Finite exterior-kernel sums on convex compact sets

This file synchronizes the exterior Cauchy-kernel approximants from ConvexRunge: every finite complex linear combination of such kernels is a compact-uniform limit of a single sequence of complex polynomials. This is the finite-quadrature closure step used in constructive Runge arguments.

theorem exists_polynomial_tendstoUniformlyOn_sum_mul_inv_sub_of_isCompact_convex {ι : Type u_1} (s : Finset ι) (coeff pole : ι → ℂ) (K : Set ℂ) (hK : IsCompact K) (hconvex : Convex ℝ K) (hpole : ∀ i ∈ s, pole i ∉ K) : ∃ (q : ℕ → Polynomial ℂ), TendstoUniformlyOn (fun (n : ℕ) (z : ℂ) => Polynomial.eval z (q n)) (fun (z : ℂ) => ∑ i ∈ s, coeff i * (pole i - z)⁻¹) Filter.atTop K

A finite complex linear combination of Cauchy kernels with poles outside a compact convex planar set is a compact-uniform limit of polynomials.