Polynomial sup norms on a domain boundary

The maximum-modulus principle identifies the polynomial sup norm on the closure of a bounded planar set with the sup norm on its frontier. A separate closure-invariance lemma identifies this compact-closure norm with the norm on the original set. This is the analytic bridge between compact closure stages in an exhaustion and the frontier-controlled smooth-domain bounds in GeneralSymmetrized.lean.

The boundedness hypothesis is explicit. Although every intended smooth convex approximation stage is bounded, SmoothJordanDomain currently stores only a compact parametrized frontier and does not expose boundedness of its carrier as a field.

Main declarations

• polynomialSupNorm_closure_eq_frontier_of_isBounded -- the general maximum-modulus identity;
• polynomialSupNorm_closure_carrier_eq_frontier -- the identity specialized to the closure of a bounded smooth Jordan carrier;
• polynomialSupNorm_closure_of_isBounded -- closure invariance on bounded sets;
• polynomialSupNorm_carrier_eq_frontier -- the direct carrier/frontier identity for a bounded smooth Jordan carrier.

theorem polynomialSupNorm_closure_eq_frontier_of_isBounded (p : Polynomial ℂ) {U : Set ℂ} (hU : Bornology.IsBounded U) : polynomialSupNorm p (closure U) = polynomialSupNorm p (frontier U)

On a bounded planar set, a polynomial's sup norm on the closure equals its sup norm on the frontier. The empty-set case is included.

theorem polynomialSupNorm_closure_carrier_eq_frontier (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hbounded : Bornology.IsBounded Omega.carrier) : polynomialSupNorm p (closure Omega.carrier) = polynomialSupNorm p (frontier Omega.carrier)

For a bounded smooth Jordan carrier, polynomial sup norms on its closure and parametrized frontier agree exactly.

theorem polynomialSupNorm_closure_of_isBounded (p : Polynomial ℂ) {X : Set ℂ} (hX : Bornology.IsBounded X) : polynomialSupNorm p (closure X) = polynomialSupNorm p X

Taking the closure of a bounded planar set does not change a polynomial's sup norm. The empty-set case is included.

theorem polynomialSupNorm_carrier_eq_frontier (Omega : SmoothJordanDomain) (p : Polynomial ℂ) (hbounded : Bornology.IsBounded Omega.carrier) : polynomialSupNorm p Omega.carrier = polynomialSupNorm p (frontier Omega.carrier)

For a bounded smooth Jordan carrier, polynomial sup norms on the carrier and its parametrized frontier agree exactly.