Complex polynomial approximation on closed disks

This file proves the disk model of the polynomial-approximation input used by the Crouzeix--Palencia smooth-exhaustion assembly. Boundary approximation is obtained by radially contracting into the open disk and taking a diagonal sequence of Taylor partial sums.

theorem SmoothJordanDomain.ball_hasMergelyanPolynomialApproximation (c : ℂ) (R : ℝ) (hR : 0 < R) : (ball c R hR).HasMergelyanPolynomialApproximation

Every complex function differentiable on an open disk and continuous on its closure is a compact-uniform limit of complex polynomials.