LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Oka-Weil approximation on a domain of holomorphy (host-domain lemma)

Statement

Assume the Axiom of Choice (AC). Let $D \subseteq C^{n}$ be a domain of holomorphy (Holomorphic extension and domains of holomorphy in several variables), let $K ⋐ D$ be compact and convex with respect to the holomorphic functions on $D$ , i.e. ${\hat{K}}_{D} = K$ (Holomorphic hulls and holomorphic convexity), and let $f$ be holomorphic in an open neighbourhood of $K$ . Then for every $ε > 0$ there is $F \in O (D)$ with $\sup_{z \in K} ∣ F (z) - f (z) ∣ < ε .$

Facts & Assumptions

Given: The Axiom of Choice; a domain $D \subseteq C^{n}$ of holomorphy; a compact $K ⋐ D$ with ${\hat{K}}_{D} = K$ ; a function $f$ holomorphic on an open neighbourhood of $K$ ; and $ε > 0$ .

[F1]

The holomorphic hull is ${\hat{E}}_{D} : = {a \in D : ∣ g (a) ∣ \leq \sup_{z \in E} ∣ g (z) ∣ for every g \in O (D)}$ (Holomorphic hulls and holomorphic convexity). Thus ${\hat{K}}_{D} = K$ is exactly the compact $O (D)$ -convexity hypothesis.

[F2]

(Harold P. Boas, Lecture Notes on Multidimensional Complex Analysis, §3.3.2, Theorem 21, printed p. 79, with proof on printed pp. 79–80.) If $G$ is a domain of holomorphy in $C^{n}$ and $K_{0} ⋐ G$ is compact and convex with respect to $O (G)$ , then every function holomorphic in a neighbourhood of $K_{0}$ is uniformly approximable on $K_{0}$ by functions in $O (G)$ . The proof uses finite analytic-polyhedron reduction, Oka's graph lift and a $\overset{ˉ}{\partial}$ correction, a power-series approximation, and a telescoping exhaustion.

[F3]

The Axiom of Choice supplies a choice function for every family of nonempty sets (The Axiom of Choice).

Choice use. AC is the ambient hypothesis recorded in the Statement and cited as [F3]. No additional choice is made in applying [F2].

Proof

technique · direct application of the cited approximation theorem

1.1F1F2given

If $K = \emptyset$ , take $F = 0$ , since the supremum of the nonnegative empty family is $0$ in the convention of [F1]. Otherwise the hypotheses of Boas's Theorem 21 [F2] hold with $G : = D$ and $K_{0} : = K$ : $D$ is a domain of holomorphy, and ${\hat{K}}_{D} = K$ is the required $O (D)$ -convexity condition by [F1]. The given $f$ is holomorphic in a neighbourhood of $K$ .

2.1F2F3step 1.1given∎

For nonempty $K$ , apply [F2] with approximation tolerance $ε$ . It gives $F \in O (D)$ with $\sup_{z \in K} ∣ F (z) - f (z) ∣ < ε$ , which is the Statement under the ambient AC assumption [F3].

Depends on

Used by

Oka-Weil approximation on a pseudoconvex domain Theorem

Dependency tree · two levels

92 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Harold P. Boas, Lecture Notes on Several Complex Variables (standard reference, not scraped)
Jean-Pierre Demailly, Complex Analytic and Differential Geometry (standard reference, not scraped)
Jiri Lebl, Tasty Bits of Several Complex Variables (standard reference, not scraped)