Holomorphic convexity of complete Reinhardt domains

An exterior point is separated from each compact subset by a monomial. The entire holomorphic hull of the compact set therefore stays in the domain. Its compactness implies compactness of the relative holomorphic hull.

Main results

exists_monomial_separator_of_isCompact separates an exterior point from a compact subset by a monomial. isHolomorphicallyConvex_of_completeReinhardt is holomorphic convexity of an open complete logarithmically convex Reinhardt domain.

theorem SeveralComplexVariables.exists_monomial_separator_of_isCompact {ι : Type u_1} [Fintype ι] {U K : Set (ι → ℂ)} (ho : IsOpen U) (hc : IsCompleteReinhardt U) (hl : IsLogarithmicallyConvex U) (hK : IsCompact K) (hKU : K ⊆ U) {z : ι → ℂ} (hz : z ∉ U) : ∃ (m : ι → ℕ) (M : ℝ), (∀ w ∈ K, ‖∏ i : ι, w i ^ m i‖ ≤ M) ∧ M < ‖∏ i : ι, z i ^ m i‖

A monomial separates a compact subset of an open complete logarithmically convex Reinhardt set from any exterior point.

theorem SeveralComplexVariables.isHolomorphicallyConvex_of_completeReinhardt {ι : Type u_1} [Fintype ι] {U : Set (ι → ℂ)} (ho : IsOpen U) (hc : IsCompleteReinhardt U) (hl : IsLogarithmicallyConvex U) : IsHolomorphicallyConvex U

Open complete logarithmically convex Reinhardt sets are holomorphically convex. This includes unbounded sets, the empty set, and empty coordinate types.