Polynomial hulls and polynomially convex sets in ℂⁿ

The polynomial hull of a set K ⊆ ℂⁿ is the set of points z at which every polynomial is bounded in modulus by any bound it satisfies on K; for compact K this is the set of z with |p(z)| ≤ max_K |p| for every polynomial p. A set is polynomially convex if it contains its polynomial hull. Polynomially convex compact sets are the natural domains of polynomial approximation in several complex variables (the Oka–Weil theorem), and the interiors of their polynomial polyhedron neighbourhoods form cofinal systems of Stein neighbourhoods, along which germs of holomorphic functions on compact sets are studied.

Points are modelled as functions ι → ℂ for a finite index type ι, polynomials as MvPolynomial ι ℂ and evaluation as MvPolynomial.eval; the norm on ι → ℂ is the sup norm, so its closed balls are closed polydiscs.

The two main results are the following.

• Every compact subset of the real locus ℝⁿ ⊆ ℂⁿ is polynomially convex. For z outside such a set K, the polynomial p(w) = 1 - ε ∑ᵢ (wᵢ - Re zᵢ)² is real on K with values in (0, 1] for small ε > 0, while p(z) = 1 + ε ∑ᵢ (Im zᵢ)²; one of the two inequalities |p| ≤ 1 ≤ |p(z)| is strict at every point of K because z ∉ K, and compactness makes the separation uniform.
• A compact polynomially convex set K has arbitrarily small polynomially convex compact neighbourhoods of the form P = closedBall 0 R ∩ ⋂ᵢ {|pᵢ| ≤ 1} for finitely many polynomials pᵢ, with K contained in the open set ball 0 R ∩ ⋂ᵢ {|pᵢ| < 1} ⊆ P. The points of the compact set closedBall 0 R \ U are separated from K by polynomials, and finitely many of these separators suffice. When K is nonempty the pᵢ can be taken nonconstant, and then this open set is exactly the interior of P: by the maximum modulus principle the modulus of a nonconstant polynomial has no local maximum, so the interior of {|p| ≤ 1} is {|p| < 1}.

Main declarations

• TauCeti.polynomialHull K: the polynomial hull of K; it contains K (TauCeti.subset_polynomialHull), is closed (TauCeti.isClosed_polynomialHull) and is idempotent (TauCeti.polynomialHull_polynomialHull).
• TauCeti.IsPolynomiallyConvex K: K contains its polynomial hull. Polynomial convexity is preserved by arbitrary intersections (TauCeti.isPolynomiallyConvex_iInter) and holds for the sublevel sets {|p| ≤ c} (TauCeti.isPolynomiallyConvex_setOfPred_norm_eval_le) and for closed balls (TauCeti.isPolynomiallyConvex_closedBall).
• TauCeti.polynomialPolyhedron R s: the polynomial polyhedron closedBall 0 R ∩ ⋂_{p ∈ s} {|p| ≤ 1}; it is compact (TauCeti.isCompact_polynomialPolyhedron) and polynomially convex (TauCeti.isPolynomiallyConvex_polynomialPolyhedron), and its interior contains ball 0 R ∩ ⋂_{p ∈ s} {|p| < 1} (TauCeti.ball_inter_biInter_subset_interior_polynomialPolyhedron), with equality when the radius is nonzero and the polynomials are nonconstant (TauCeti.interior_polynomialPolyhedron).

Main results

• TauCeti.exists_norm_eval_lt_one_lt_of_notMem_polynomialHull: a point outside the hull of K is separated from K by a polynomial of modulus < 1 on K and > 1 at the point.
• TauCeti.isPolynomiallyConvex_iff_forall_notMem_exists_norm_eval_lt_one_lt: K is polynomially convex if and only if every point outside K is separated from K in this way.
• IsCompact.notMem_polynomialHull_of_forall_norm_eval_lt: if |p| < |p(z)| at every point of a compact K, then z is not in the hull of K.
• IsCompact.isPolynomiallyConvex_of_forall_im_eq_zero: compact subsets of ℝⁿ are polynomially convex.
• TauCeti.IsPolynomiallyConvex.exists_polynomialPolyhedron_subset: the polynomial polyhedron neighbourhoods of a compact polynomially convex set, and TauCeti.IsPolynomiallyConvex.exists_subset_interior_polynomialPolyhedron: such a set lies in the interior of a polynomial polyhedron inside any given open neighbourhood.
• TauCeti.IsPolynomiallyConvex.exists_polynomialPolyhedron_subset_of_nonempty: for nonempty K, the polynomial polyhedron neighbourhoods can be cut out by nonconstant polynomials.
• TauCeti.interior_setOfPred_norm_eval_le: the interior of {|p| ≤ c} is {|p| < c} for a nonconstant polynomial p.

References

• L. Hörmander, An introduction to complex analysis in several variables, 3rd ed., North-Holland, 1990, §2.7.
• E. L. Stout, Polynomial convexity, Progress in Mathematics 261, Birkhäuser, 2007, Chapter 1.

def TauCeti.polynomialHull {ι : Type u_1} (K : Set (ι → ℂ)) : Set (ι → ℂ)

The polynomial hull of a set K ⊆ ℂⁿ: the points z such that |p(z)| ≤ c for every polynomial p and every bound c with |p| ≤ c on K. For compact K these are the points with |p(z)| ≤ max_K |p| for every polynomial p.

def TauCeti.IsPolynomiallyConvex {ι : Type u_1} (K : Set (ι → ℂ)) : Prop

A set K ⊆ ℂⁿ is polynomially convex if it contains its polynomial hull. For compact K this is the standard notion; for unbounded K it is stricter than the convention that the hull of every compact subset of K stays in K (for instance, ℝⁿ with n ≥ 1 is not polynomially convex in this sense, since only constant polynomials are bounded on it).

theorem TauCeti.isPolynomiallyConvex_iff {ι : Type u_1} {K : Set (ι → ℂ)} : IsPolynomiallyConvex K ↔ polynomialHull K ⊆ K

theorem TauCeti.mem_polynomialHull_iff {ι : Type u_1} {K : Set (ι → ℂ)} {z : ι → ℂ} : z ∈ polynomialHull K ↔ ∀ (p : MvPolynomial ι ℂ) (c : ℝ), (∀ w ∈ K, ‖(MvPolynomial.eval w) p‖ ≤ c) → ‖(MvPolynomial.eval z) p‖ ≤ c

theorem TauCeti.subset_polynomialHull {ι : Type u_1} (K : Set (ι → ℂ)) : K ⊆ polynomialHull K

theorem TauCeti.polynomialHull_mono {ι : Type u_1} {K L : Set (ι → ℂ)} (h : K ⊆ L) : polynomialHull K ⊆ polynomialHull L

@[simp]

theorem TauCeti.polynomialHull_empty {ι : Type u_1} : polynomialHull ∅ = ∅

@[simp]

theorem TauCeti.polynomialHull_polynomialHull {ι : Type u_1} (K : Set (ι → ℂ)) : polynomialHull (polynomialHull K) = polynomialHull K

Taking the polynomial hull is idempotent.

theorem TauCeti.isClosed_polynomialHull {ι : Type u_1} (K : Set (ι → ℂ)) : IsClosed (polynomialHull K)

The polynomial hull of any set is closed.

theorem TauCeti.exists_norm_eval_lt_one_lt_of_notMem_polynomialHull {ι : Type u_1} {K : Set (ι → ℂ)} {z : ι → ℂ} (hz : z ∉ polynomialHull K) : ∃ (p : MvPolynomial ι ℂ), (∀ w ∈ K, ‖(MvPolynomial.eval w) p‖ < 1) ∧ 1 < ‖(MvPolynomial.eval z) p‖

A point outside the polynomial hull of K is separated from K by a polynomial: there is p with |p| < 1 on K and |p(z)| > 1.

theorem IsCompact.notMem_polynomialHull_of_forall_norm_eval_lt {ι : Type u_1} {K : Set (ι → ℂ)} {z : ι → ℂ} (hK : IsCompact K) {p : MvPolynomial ι ℂ} (hp : ∀ w ∈ K, ‖(MvPolynomial.eval w) p‖ < ‖(MvPolynomial.eval z) p‖) : z ∉ TauCeti.polynomialHull K

If a polynomial is strictly smaller in modulus at every point of a compact set K than at z, then z is not in the polynomial hull of K.

theorem TauCeti.isPolynomiallyConvex_iff_polynomialHull_eq {ι : Type u_1} {K : Set (ι → ℂ)} : IsPolynomiallyConvex K ↔ polynomialHull K = K

theorem TauCeti.isPolynomiallyConvex_polynomialHull {ι : Type u_1} (K : Set (ι → ℂ)) : IsPolynomiallyConvex (polynomialHull K)

theorem TauCeti.IsPolynomiallyConvex.exists_norm_eval_lt_one_lt {ι : Type u_1} {K : Set (ι → ℂ)} {z : ι → ℂ} (hK : IsPolynomiallyConvex K) (hz : z ∉ K) : ∃ (p : MvPolynomial ι ℂ), (∀ w ∈ K, ‖(MvPolynomial.eval w) p‖ < 1) ∧ 1 < ‖(MvPolynomial.eval z) p‖

A point outside a polynomially convex set K is separated from K by a polynomial of modulus < 1 on K and > 1 at the point.

theorem TauCeti.isPolynomiallyConvex_iff_forall_notMem_exists_norm_eval_lt_one_lt {ι : Type u_1} {K : Set (ι → ℂ)} : IsPolynomiallyConvex K ↔ ∀ z ∉ K, ∃ (p : MvPolynomial ι ℂ), (∀ w ∈ K, ‖(MvPolynomial.eval w) p‖ < 1) ∧ 1 < ‖(MvPolynomial.eval z) p‖

A set K is polynomially convex if and only if every point outside K is separated from K by a polynomial of modulus < 1 on K and > 1 at the point.

theorem TauCeti.isPolynomiallyConvex_empty {ι : Type u_1} : IsPolynomiallyConvex ∅

theorem TauCeti.isPolynomiallyConvex_iInter {ι : Type u_1} {κ : Sort u_2} {K : κ → Set (ι → ℂ)} (hK : ∀ (k : κ), IsPolynomiallyConvex (K k)) : IsPolynomiallyConvex (⋂ (k : κ), K k)

An intersection of polynomially convex sets is polynomially convex.

theorem TauCeti.IsPolynomiallyConvex.inter {ι : Type u_1} {K L : Set (ι → ℂ)} (hK : IsPolynomiallyConvex K) (hL : IsPolynomiallyConvex L) : IsPolynomiallyConvex (K ∩ L)

The intersection of two polynomially convex sets is polynomially convex.

theorem TauCeti.isPolynomiallyConvex_setOfPred_norm_eval_le {ι : Type u_1} (p : MvPolynomial ι ℂ) (c : ℝ) : IsPolynomiallyConvex {w : ι → ℂ | ‖(MvPolynomial.eval w) p‖ ≤ c}

A sublevel set {w | |p(w)| ≤ c} of the modulus of a polynomial is polynomially convex.

theorem TauCeti.interior_setOfPred_norm_eval_le {ι : Type u_1} [Finite ι] {p : MvPolynomial ι ℂ} (hp : p.totalDegree ≠ 0) (c : ℝ) : interior {w : ι → ℂ | ‖(MvPolynomial.eval w) p‖ ≤ c} = {w : ι → ℂ | ‖(MvPolynomial.eval w) p‖ < c}

The interior of a sublevel set {w | |p(w)| ≤ c} of the modulus of a nonconstant polynomial p is the strict sublevel set {w | |p(w)| < c}.

theorem TauCeti.isPolynomiallyConvex_closedBall {ι : Type u_1} [Fintype ι] (x : ι → ℂ) (r : ℝ) : IsPolynomiallyConvex (Metric.closedBall x r)

Closed balls of ℂⁿ for the sup norm, that is, closed polydiscs, are polynomially convex.

theorem IsCompact.isPolynomiallyConvex_of_forall_im_eq_zero {ι : Type u_1} {K : Set (ι → ℂ)} [Finite ι] (hK : IsCompact K) (hreal : ∀ w ∈ K, ∀ (i : ι), (w i).im = 0) : TauCeti.IsPolynomiallyConvex K

Every compact subset of the real locus ℝⁿ ⊆ ℂⁿ is polynomially convex.

noncomputable def TauCeti.polynomialPolyhedron {ι : Type u_1} [Fintype ι] (R : ℝ) (s : Finset (MvPolynomial ι ℂ)) : Set (ι → ℂ)

The polynomial polyhedron closedBall 0 R ∩ ⋂_{p ∈ s} {|p| ≤ 1} cut out of the closed polydisc of radius R by a finite set s of polynomials.

@[simp]

theorem TauCeti.mem_polynomialPolyhedron_iff {ι : Type u_1} [Fintype ι] {R : ℝ} {s : Finset (MvPolynomial ι ℂ)} {w : ι → ℂ} : w ∈ polynomialPolyhedron R s ↔ ‖w‖ ≤ R ∧ ∀ p ∈ s, ‖(MvPolynomial.eval w) p‖ ≤ 1

theorem TauCeti.isClosed_polynomialPolyhedron {ι : Type u_1} [Fintype ι] (R : ℝ) (s : Finset (MvPolynomial ι ℂ)) : IsClosed (polynomialPolyhedron R s)

theorem TauCeti.isCompact_polynomialPolyhedron {ι : Type u_1} [Fintype ι] (R : ℝ) (s : Finset (MvPolynomial ι ℂ)) : IsCompact (polynomialPolyhedron R s)

theorem TauCeti.ball_inter_biInter_subset_interior_polynomialPolyhedron {ι : Type u_1} [Fintype ι] (R : ℝ) (s : Finset (MvPolynomial ι ℂ)) : Metric.ball 0 R ∩ ⋂ p ∈ s, {w : ι → ℂ | ‖(MvPolynomial.eval w) p‖ < 1} ⊆ interior (polynomialPolyhedron R s)

The open set ball 0 R ∩ ⋂_{p ∈ s} {|p| < 1} lies in the interior of the polynomial polyhedron polynomialPolyhedron R s.

theorem TauCeti.isPolynomiallyConvex_polynomialPolyhedron {ι : Type u_1} [Fintype ι] (R : ℝ) (s : Finset (MvPolynomial ι ℂ)) : IsPolynomiallyConvex (polynomialPolyhedron R s)

Polynomial polyhedra are polynomially convex.

theorem TauCeti.interior_polynomialPolyhedron {ι : Type u_1} [Fintype ι] {R : ℝ} {s : Finset (MvPolynomial ι ℂ)} (hR : R ≠ 0) (hs : ∀ p ∈ s, p.totalDegree ≠ 0) : interior (polynomialPolyhedron R s) = Metric.ball 0 R ∩ ⋂ p ∈ s, {w : ι → ℂ | ‖(MvPolynomial.eval w) p‖ < 1}

The interior of a polynomial polyhedron closedBall 0 R ∩ ⋂_{p ∈ s} {|p| ≤ 1} of nonzero radius whose defining polynomials are nonconstant is ball 0 R ∩ ⋂_{p ∈ s} {|p| < 1}.

theorem TauCeti.IsPolynomiallyConvex.exists_polynomialPolyhedron_subset {ι : Type u_1} {K : Set (ι → ℂ)} [Fintype ι] (hKc : IsPolynomiallyConvex K) (hK : IsCompact K) {U : Set (ι → ℂ)} (hU : IsOpen U) (hKU : K ⊆ U) : ∃ (R : ℝ) (s : Finset (MvPolynomial ι ℂ)), 0 < R ∧ K ⊆ Metric.ball 0 R ∩ ⋂ p ∈ s, {w : ι → ℂ | ‖(MvPolynomial.eval w) p‖ < 1} ∧ polynomialPolyhedron R s ⊆ U

Polynomial polyhedron neighbourhoods. A compact polynomially convex set K ⊆ ℂⁿ with an open neighbourhood U has a polynomial polyhedron neighbourhood P = closedBall 0 R ∩ ⋂_{p ∈ s} {|p| ≤ 1} inside U, for a radius R > 0 and a finite set s of polynomials, such that K lies in the open subset ball 0 R ∩ ⋂_{p ∈ s} {|p| < 1} of P. The set P is compact (TauCeti.isCompact_polynomialPolyhedron) and polynomially convex (TauCeti.isPolynomiallyConvex_polynomialPolyhedron).

theorem TauCeti.IsPolynomiallyConvex.exists_subset_interior_polynomialPolyhedron {ι : Type u_1} {K : Set (ι → ℂ)} [Fintype ι] (hKc : IsPolynomiallyConvex K) (hK : IsCompact K) {U : Set (ι → ℂ)} (hU : IsOpen U) (hKU : K ⊆ U) : ∃ (R : ℝ) (s : Finset (MvPolynomial ι ℂ)), 0 < R ∧ K ⊆ interior (polynomialPolyhedron R s) ∧ polynomialPolyhedron R s ⊆ U

A compact polynomially convex set K ⊆ ℂⁿ lies in the interior of a polynomial polyhedron contained in any given open neighbourhood U of K.

theorem TauCeti.IsPolynomiallyConvex.exists_polynomialPolyhedron_subset_of_nonempty {ι : Type u_1} {K : Set (ι → ℂ)} [Fintype ι] (hKc : IsPolynomiallyConvex K) (hK : IsCompact K) (hKne : K.Nonempty) {U : Set (ι → ℂ)} (hU : IsOpen U) (hKU : K ⊆ U) : ∃ (R : ℝ) (s : Finset (MvPolynomial ι ℂ)), 0 < R ∧ (∀ p ∈ s, p.totalDegree ≠ 0) ∧ K ⊆ Metric.ball 0 R ∩ ⋂ p ∈ s, {w : ι → ℂ | ‖(MvPolynomial.eval w) p‖ < 1} ∧ polynomialPolyhedron R s ⊆ U

Polynomial polyhedron neighbourhoods with nonconstant polynomials. A nonempty compact polynomially convex set K ⊆ ℂⁿ with an open neighbourhood U has a polynomial polyhedron neighbourhood P = closedBall 0 R ∩ ⋂_{p ∈ s} {|p| ≤ 1} inside U, for a radius R > 0 and a finite set s of nonconstant polynomials, such that K lies in the open subset ball 0 R ∩ ⋂_{p ∈ s} {|p| < 1} of P; this open subset is the interior of P (TauCeti.interior_polynomialPolyhedron).