Polynomial approximation from smooth-Jordan Cauchy formulas

This file converts a normalized scalar Cauchy formula on a compact smooth convex Jordan carrier into uniform polynomial approximation on its closure. Strict radial contraction moves the evaluation point into the carrier and turns each boundary kernel into one whose pole lies strictly outside the closed carrier. ConvexRungeIntegral approximates each radialized function, and a diagonal selection removes the radial contraction.

noncomputable def smoothJordanRadialPoint (c z : ℂ) (r : ℝ) : ℂ

The strict radial contraction of z toward c.

Equations

• smoothJordanRadialPoint c z r = (1 - r) • c + r • z

noncomputable def smoothJordanOutwardPoint (c xi : ℂ) (r : ℝ) : ℂ

The point beyond xi on the ray from c, reciprocal to the radial contraction factor.

Equations

• smoothJordanOutwardPoint c xi r = c + r⁻¹ • (xi - c)

theorem SmoothJordanDomain.smoothJordanOutwardPoint_not_mem_closure (Omega : SmoothJordanDomain) {c xi : ℂ} (hc : c ∈ Omega.carrier) (hxi : xi ∈ frontier Omega.carrier) {r : ℝ} (hr : r ∈ Set.Ioo 0 1) : smoothJordanOutwardPoint c xi r ∉ closure Omega.carrier

A boundary point pushed outward by the reciprocal of a strict radial contraction lies outside the closed convex carrier.

theorem SmoothJordanDomain.smoothJordanRadialPoint_mem_carrier (Omega : SmoothJordanDomain) {c z : ℂ} (hc : c ∈ Omega.carrier) (hz : z ∈ closure Omega.carrier) {r : ℝ} (hr : r ∈ Set.Ioo 0 1) : smoothJordanRadialPoint c z r ∈ Omega.carrier

Strict radial contractions of points in the closed carrier lie in its open interior.

theorem SmoothJordanDomain.hasMergelyanPolynomialApproximation_of_intervalCauchyFormula (Omega : SmoothJordanDomain) (hcompact : IsCompact (closure Omega.carrier)) (hCauchy : ∀ (f : ℂ → ℂ), DiffContOnCl ℂ f Omega.carrier → ∀ z ∈ Omega.carrier, f z = ∫ (t : ℝ) in 0..2 * Real.pi, (2 * ↑Real.pi * Complex.I)⁻¹ * deriv Omega.boundaryParam t * f (Omega.boundaryParam t) * (Omega.boundaryParam t - z)⁻¹) : Omega.HasMergelyanPolynomialApproximation

A normalized interval Cauchy formula on a compact smooth convex Jordan carrier implies the full polynomial approximation property.

theorem SmoothJordanDomain.hasMergelyanPolynomialApproximation_of_cauchyFormula (Omega : SmoothJordanDomain) (hcompact : IsCompact (closure Omega.carrier)) (hCauchy : ∀ (f : ℂ → ℂ), DiffContOnCl ℂ f Omega.carrier → ∀ z ∈ Omega.carrier, f z = (2 * ↑Real.pi * Complex.I)⁻¹ * contourIntegral (fun (xi : ℂ) => f xi * (xi - z)⁻¹) Omega.boundaryParam) : Omega.HasMergelyanPolynomialApproximation

The contour form of the normalized Cauchy formula implies the same polynomial approximation property.

theorem SmoothJordanDomain.hasMergelyanPolynomialApproximation (Omega : SmoothJordanDomain) : Omega.HasMergelyanPolynomialApproximation

Every smooth strictly convex Jordan domain has the polynomial approximation property on its closed carrier.