Polynomial sup-norms on approximating boundaries

The explicit open thickenings from SmoothApprox.lean and the closed thickenings from CompactThickeningApprox.lean use the same radius at every stage. The closure of the open thickening is exactly the closed thickening. The maximum-modulus transfer in BoundaryMaximum.lean therefore identifies the polynomial sup-norm on the open-stage frontier with the norm on the compact control set.

Consequently, for a compact target, these frontier sup-norms converge to the sup-norm on the target. This is the scalar limit needed when a smooth-boundary estimate is passed through the compact exhaustion.

Main declarations

• polynomialSupNorm_frontier_convexThickeningApprox_eq_compactThickeningApprox identifies the boundary and compact-stage norms.
• tendsto_polynomialSupNorm_frontier_convexThickeningApprox_atTop proves convergence of the boundary norms to the target norm.

theorem polynomialSupNorm_frontier_convexThickeningApprox_eq_compactThickeningApprox (p : Polynomial ℂ) {K : Set ℂ} (hK : Bornology.IsBounded K) (n : ℕ) : polynomialSupNorm p (frontier (convexThickeningApprox K n)) = polynomialSupNorm p (compactThickeningApprox K n)

For a bounded set, the polynomial sup-norm on the frontier of its open thickening equals the norm on the closed thickening at the same radius.

theorem tendsto_polynomialSupNorm_frontier_convexThickeningApprox_atTop (p : Polynomial ℂ) {K : Set ℂ} (hK : IsCompact K) : Filter.Tendsto (fun (n : ℕ) => polynomialSupNorm p (frontier (convexThickeningApprox K n))) Filter.atTop (nhds (polynomialSupNorm p K))

For a compact target, polynomial sup-norms on the frontiers of the explicit open thickenings converge to the target sup-norm.