Polynomial approximation of exterior Cauchy kernels on convex sets

This file proves the elementary Runge input needed for convex planar compact sets: a Cauchy kernel whose pole lies off the set is a compact-uniform limit of complex polynomials. Strict Hahn--Banach separation supplies an affine contraction, and its geometric series gives the approximating polynomials.

exists_polynomial_separator_of_isCompact_nonempty_convex exposes the underlying affine separator directly for downstream polynomial-hull and functional-calculus arguments.

theorem exists_polynomial_separator_of_isCompact_nonempty_convex (K : Set ℂ) (hK : IsCompact K) (hne : K.Nonempty) (hconvex : Convex ℝ K) {ζ : ℂ} (hζ : ζ ∉ K) : ∃ (p : Polynomial ℂ) (r : ℝ), 0 ≤ r ∧ r < 1 ∧ Polynomial.eval ζ p = 1 ∧ ∀ z ∈ K, ‖Polynomial.eval z p‖ ≤ r

A point outside a nonempty compact convex planar set can be separated in modulus by an affine complex polynomial: the polynomial takes value one at the exterior point and has norm uniformly bounded by some r < 1 on the set.

theorem exists_polynomial_tendstoUniformlyOn_inv_sub_of_isCompact_convex (K : Set ℂ) (hK : IsCompact K) (hconvex : Convex ℝ K) {ζ : ℂ} (hζ : ζ ∉ K) : ∃ (q : ℕ → Polynomial ℂ), TendstoUniformlyOn (fun (n : ℕ) (z : ℂ) => Polynomial.eval z (q n)) (fun (z : ℂ) => (ζ - z)⁻¹) Filter.atTop K

On a compact convex planar set, every Cauchy kernel with exterior pole is a compact-uniform limit of complex polynomials.