Common extension domains inside a complex vector space

IsCommonAnalyticExtension U V says that U ⊆ V and every scalar analytic function on U extends to V. It does not impose openness, connectedness, or maximality, and does not define an abstract envelope. Simultaneous extension cannot introduce new scalar values, by extending the reciprocal of a nowhere-zero function.

Convex separation also bounds common extension domains by the real convex hull. References: [Korevaar–Wiegerinck][KorevaarWiegerinck2017] (2017), Proposition 2.9.2 and Corollary 2.9.3, specialized to domains in a complex normed space.

Main definitions

• IsCommonAnalyticExtension: Every scalar analytic function on U extends to the larger set V.

Main results

• IsCommonAnalyticExtension.trans: Common extension composes.
• IsCommonAnalyticExtension.image_eq: A scalar analytic function on a connected common extension domain has exactly its original range.
• IsCommonAnalyticExtension.subset_convexHull: A common extension domain lies in the real convex hull of the original domain.

References

• [J. Korevaar and J. Wiegerinck, Several Complex Variables][KorevaarWiegerinck2017]

def SeveralComplexVariables.IsCommonAnalyticExtension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U V : Set E) : Prop

Every scalar analytic function on U extends to the larger set V. Topological hypotheses and maximality are separate; no extension outside the ambient space is intended.

Equations

• SeveralComplexVariables.IsCommonAnalyticExtension U V = (U ⊆ V ∧ ∀ (f : E → ℂ), AnalyticOnNhd ℂ f U → ∃ (g : E → ℂ), AnalyticOnNhd ℂ g V ∧ Set.EqOn g f U)

theorem SeveralComplexVariables.isCommonAnalyticExtension_of_forall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U V : Set E} (hUV : U ⊆ V) (he : ∀ (f : E → ℂ), AnalyticOnNhd ℂ f U → ∃ (g : E → ℂ), AnalyticOnNhd ℂ g V ∧ Set.EqOn g f U) : IsCommonAnalyticExtension U V

Construct a common extension property from containment and extension of each scalar analytic function.

theorem SeveralComplexVariables.IsCommonAnalyticExtension.subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U V : Set E} (h : IsCommonAnalyticExtension U V) : U ⊆ V

A common extension pair includes the original set in the extension set.

theorem SeveralComplexVariables.IsCommonAnalyticExtension.exists_extension {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U V : Set E} (h : IsCommonAnalyticExtension U V) {f : E → ℂ} (hf : AnalyticOnNhd ℂ f U) : ∃ (g : E → ℂ), AnalyticOnNhd ℂ g V ∧ Set.EqOn g f U

Apply a common extension property to a scalar analytic function.

theorem SeveralComplexVariables.isCommonAnalyticExtension_refl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U : Set E) : IsCommonAnalyticExtension U U

Every set is a common extension domain for itself.

theorem SeveralComplexVariables.IsCommonAnalyticExtension.trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U V W : Set E} (hUV : IsCommonAnalyticExtension U V) (hVW : IsCommonAnalyticExtension V W) : IsCommonAnalyticExtension U W

Common extension composes.

theorem SeveralComplexVariables.IsCommonAnalyticExtension.ne_on {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U V : Set E} (h : IsCommonAnalyticExtension U V) (ho : IsOpen U) (hne : U.Nonempty) (hc : IsPreconnected V) {f : E → ℂ} (hf : AnalyticOnNhd ℂ f V) {c : ℂ} (hno : ∀ z ∈ U, f z ≠ c) (z : E) : z ∈ V → f z ≠ c

An omitted scalar value remains omitted on a connected common extension domain.

theorem SeveralComplexVariables.IsCommonAnalyticExtension.image_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U V : Set E} (h : IsCommonAnalyticExtension U V) (ho : IsOpen U) (hne : U.Nonempty) (hc : IsPreconnected V) {f : E → ℂ} (hf : AnalyticOnNhd ℂ f V) : f '' V = f '' U

A scalar analytic function on a connected common extension domain has exactly its original range. This is the Euclidean version of Proposition 2.9.2.

theorem SeveralComplexVariables.IsCommonAnalyticExtension.subset_convexHull {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U V : Set E} (h : IsCommonAnalyticExtension U V) (ho : IsOpen U) (hne : U.Nonempty) (hc : IsPreconnected V) : V ⊆ (convexHull ℝ) U

A common extension domain lies in the real convex hull of the original domain. The proof uses real convex separation, complexification of the separating functional, and preservation of omitted values. This assertion involves no abstract envelopes.