LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

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.

Sup-norm and first-derivative bounds by the $L^{2}$ norm on compact subsets

Facts & Assumptions

Given: $m \geq 1$ , the Axiom of Countable Choice ${A C}_{ω}$ , an open set $Ω \subseteq C^{m}$ , a nonempty compact set $K \subseteq Ω$ , and a holomorphic function $f \in L^{2} (Ω)$ .

[A1]

The only choice principle is ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). It is used through the local mean-value lemma and the complex $L^{2}$ Hilbert-space supplier; no full Axiom of Choice or sequence-selection principle is used.

[F1]

Read $C^{m}$ as $R^{2 m}$ with its Euclidean metric and norm (Complex $m$ -space and its real coordinate dictionary).

[F2]

Open and closed polydiscs and balls have the coordinatewise definitions of Balls, polydiscs and the distinguished boundary in $C^{m}$ .

[F3]

For a holomorphic $g$ on an open set containing a closed polydisc ${\overline{Δ}}_{r} (a)$ , the local mean-value lemma gives $∣ g (a) ∣ \leq (π^{m} \prod_{j < m} r_{j}^{2})^{- 1 / 2} ∥ g ∥_{L^{2} (Δ_{r} (a))}$ (The mean-value $L^{2}$ bound for holomorphic functions on a polydisc).

[F4]

If $g$ is holomorphic on $Δ_{ρ} (a)$ , $r_{j} < ρ_{j}$ , and $M = \sup_{Γ_{r} (a)} ∣ g ∣$ , then $∣ \partial_{z}^{α} g (a) ∣ \leq α! M \prod_{j < m} r_{j}^{- α_{j}}$ (Cauchy estimates for mixed derivatives on a polydisc).

[F5]

Holomorphic functions on open subsets of $C^{m}$ are continuous (Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic).

[F6]

Multi-index notation and $\partial^{0} f = f$ use the convention of $C^{k}$ maps and multi-index derivative notation in Euclidean space.

[F7]

Under ${A C}_{ω}$ , complex $L^{2} (Ω)$ with its quotient norm is a Hilbert space, so the norm satisfies the triangle inequality and convergence implies the Cauchy property ( $L^{2}$ with the integral pairing is a Hilbert space, Complex Lp classes and Euclidean test-function conventions).

[F8]

If $0 \leq g \leq h$ are measurable, then $\int g \leq \int h$ (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F9]

In a metric space, distance to a nonempty set is $1$ -Lipschitz and hence continuous by the $ε$ - $δ$ definition (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, $∣ d (x, A) - d (y, A) ∣ \leq d (x, y)$ , so the distance to a fixed nonempty set is $1$ -Lipschitz, Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form).

[F10]

In a metric space, openness gives a ball about each point (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space).

[F11]

A compact subset is compact in its subspace metric, and a continuous real-valued function on a nonempty compact metric space attains its minimum (A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F12]

Every Euclidean closed ball of positive radius in $R^{2 m}$ is compact (For $n \geq 1$ , every Euclidean closed ball and every Euclidean sphere of positive radius is compact).

[F13]

A Cauchy sequence in $C$ converges (The complex plane is complete, and convergence is equivalent to convergence of real and imaginary parts).

[F14]

A locally uniform limit of holomorphic functions is holomorphic with locally uniform convergence of every complex derivative (Locally uniform limits of holomorphic functions are holomorphic, with locally uniform convergence of all derivatives).

[F15]

For nonnegative measurable functions, Fatou's lemma gives $\int lim inf g_{n} \leq lim inf \int g_{n}$ (Fatou's lemma).

[F16]

Sums and scalar multiples of holomorphic functions are holomorphic (Sums, products and nonvanishing quotients of holomorphic functions are holomorphic).

Statement

Assume ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $m \geq 1$ , let $Ω \subseteq C^{m}$ be open, and let $K \subseteq Ω$ be nonempty and compact. There are finite constants $C_{K}$ and $C_{K, α}$ for every multi-index $α$ with $∣ α ∣ \leq 1$ such that every holomorphic $f \in L^{2} (Ω)$ satisfies

$\sup_{z \in K} ∣ f (z) ∣ \leq C_{K} ∥ f ∥_{L^{2} (Ω)}, \sup_{z \in K} ∣ \partial_{z}^{α} f (z) ∣ \leq C_{K, α} ∥ f ∥_{L^{2} (Ω)} .$

Moreover, if a sequence of holomorphic $L^{2} (Ω)$ functions $(f_{n})$ converges in $L^{2} (Ω)$ to an equivalence class $g$ , then $g$ has a holomorphic representative $F$ and $f_{n} \to F$ , $\partial_{z}^{α} f_{n} \to \partial_{z}^{α} F$ uniformly on $K$ for every $∣ α ∣ \leq 1$ .

Proof

technique · direct, combining a local mean-value estimate with polydisc Cauchy estimates

Given: $m, Ω, K, f$ as in the statement.

1.1F1F9F10F11given

If $Ω^{c} = \emptyset$ , set $δ = 1$ . Otherwise put $q (z) = d (z, Ω^{c})$ . By [F9] this is continuous, and for each $z \in K$ openness gives an $ε_{z} > 0$ with $B (z, ε_{z}) \subseteq Ω$ , so $q (z) \geq ε_{z} > 0$ . The minimum $d_{0} = \min_{z \in K} q (z)$ is positive by [F11]; set $δ = \min {1, d_{0}}$ . In either case, $\overline{B} (z, δ / 2) \subseteq Ω$ for every $z \in K$ . Let $r = δ / (4 \sqrt{m}) > 0$ .

2.1A1F1F2F3F7F8step 1.1given

For $z \in K$ the closed polydisc ${\overline{Δ}}_{2 r} (z)$ is contained in $\overline{B} (z, δ / 2)$ , since each coordinate difference is at most $2 r$ and $2 \sqrt{m} r = δ / 2$ . If $ζ \in Γ_{r} (z)$ , each coordinate of a point in ${\overline{Δ}}_{r} (ζ)$ differs from $z$ by at most $2 r$ as well, so ${\overline{Δ}}_{r} (ζ) \subseteq \overline{B} (z, δ / 2)$ . Thus these closed polydiscs lie in $Ω$ . For each such $ζ$ , the local mean bound [F3], monotonicity [F8], and the $L^{2}$ norm definition in [F7] give $∣ f (ζ) ∣^{2} \leq (π r^{2})^{- m} \int_{Δ_{r} (ζ)} ∣ f ∣^{2} \leq (π r^{2})^{- m} ∥ f ∥_{L^{2} (Ω)}^{2}$ , so $\sup_{ζ \in Γ_{r} (z)} ∣ f (ζ) ∣ \leq (π r^{2})^{- m / 2} ∥ f ∥_{L^{2} (Ω)}$ .

3.1F2F4F6step 2.1given

Since $f$ is holomorphic on $Δ_{2 r} (z)$ and $r < 2 r$ , apply [F4] with outer polyradius $2 r$ and inner polyradius $r$ . For every $∣ α ∣ \leq 1$ this gives $∣ \partial_{z}^{α} f (z) ∣ \leq α! r^{- ∣ α ∣} (π r^{2})^{- m / 2} ∥ f ∥_{L^{2} (Ω)}$ . This includes $α = 0$ , where $\partial_{z}^{0} f = f$ by [F6].

4.1step 3.1givenalgebra

Taking $C_{K} = (π r^{2})^{- m / 2}$ and $C_{K, α} = α! r^{- ∣ α ∣} (π r^{2})^{- m / 2}$ in step 3.1 proves both compact estimates.

5.1A1F1F7F10F12F13F16step 4.1given

Now let $(f_{n})$ converge in $L^{2} (Ω)$ to $g$ . By [F7] it is Cauchy in that norm. For every nonempty compact $K^{'} \subseteq Ω$ , applying the first estimate of step 4.1 to the holomorphic $L^{2}$ difference $f_{n} - f_{k}$ (holomorphic by [F16]) shows that $(f_{n})$ is uniformly Cauchy on $K^{'}$ . Every point of $Ω$ has an open ball neighborhood contained in $Ω$ by [F10]; its concentric closed ball of half the radius is compact by [F12]. Completeness of $C$ in [F13] therefore gives a pointwise limit $F$ on $Ω$ , and letting $k \to \infty$ in the uniform Cauchy bound shows $f_{n} \to F$ uniformly on every compact subset of $Ω$ .

6.1F6F14step 5.1

The convergence in step 5.1 is locally uniform, so [F14] implies that $F$ is holomorphic and that $\partial_{z}^{α} f_{n} \to \partial_{z}^{α} F$ locally uniformly for every multi-index $α$ . In particular this convergence is uniform on the compact set $K$ for $∣ α ∣ \leq 1$ .

7.1A1F5F7F15step 5.1step 6.1given∎

To identify the $L^{2}$ limit, fix $ε > 0$ and choose $N$ so that $∥ f_{n} - f_{k} ∥_{L^{2} (Ω)} < ε$ whenever $n, k \geq N$ , using convergence to $g$ and [F7]. For fixed $n \geq N$ , $f_{k} (z) \to F (z)$ pointwise; the functions are measurable since $f_{n}$ and the holomorphic $F$ are continuous by [F5]. Fatou's lemma [F15] applied to $∣ f_{n} - f_{k} ∣^{2}$ gives $∥ f_{n} - F ∥_{L^{2} (Ω)}^{2} \leq {lim inf}_{k \to \infty} ∥ f_{n} - f_{k} ∥_{L^{2} (Ω)}^{2} \leq ε^{2}$ . Thus $f_{n} - F \in L^{2} (Ω)$ , and the vector-space property in [F7] gives $F \in L^{2} (Ω)$ ; the same estimate for all $n \geq N$ proves $f_{n} \to F$ in $L^{2} (Ω)$ . Uniqueness of limits in the norm metric gives $[F] = g$ .

Depends on

Used by

Dependency tree · two levels

135 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

Jiří Lebl, Tasty Bits of Several Complex Variables (standard reference, not scraped)
Zbigniew Błocki, The Bergman Kernel and Metric (standard reference, not scraped)

Sup-norm and first-derivative bounds by the L2L2 norm on compact subsets