TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Reproducing property, Bergman projection and the extremal characterization

Statement

Assume ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), let $m \geq 1$ , and let $Ω \subseteq C^{m}$ be a nonempty open set. Write $k_{w} = K_{Ω} (\cdot, w)$ for the Riesz section at $w \in Ω$ , and let $P : L^{2} (Ω) \to A^{2} (Ω)$ be the Hilbert orthogonal projection. Then for every $w \in Ω$ :

For every $f \in A^{2} (Ω)$ , $f (w) = ⟨ f, k_{w} ⟩ = \int_{Ω} f (z) \overline{K_{Ω} (z, w)} d λ_{Ω} (z)$ .
For every $f \in L^{2} (Ω)$ , $P f (w) = ⟨ f, k_{w} ⟩ = \int_{Ω} f (z) \overline{K_{Ω} (z, w)} d λ_{Ω} (z)$ ; $P$ is linear, self-adjoint and contractive, and $P f = f$ for $f \in A^{2} (Ω)$ .
$K_{Ω} (w, w) = ∥ k_{w} ∥_{2}^{2} = \sup {∣ f (w) ∣^{2} : f \in A^{2} (Ω), ∥ f ∥_{2} \leq 1}$ and $∣ f (w) ∣^{2} \leq K_{Ω} (w, w) ∥ f ∥_{2}^{2}$ for every $f \in A^{2} (Ω)$ . If $k_{w} \neq 0$ , the maximizers in the supremum are exactly $λ k_{w} / ∥ k_{w} ∥_{2}$ with $∣ λ ∣ = 1$ ; if $k_{w} = 0$ , every member of the closed unit ball attains the supremum, which is $0$ .

Facts & Assumptions

[A1]

The only choice principle is ${A C}_{ω}$ , inherited through the Bergman Hilbert-space structure and the orthogonal-decomposition and projection suppliers; no full Axiom of Choice is used (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

$A^{2} (Ω)$ is a closed complex linear subspace of the Hilbert space $L^{2} (Ω)$ , with the first-variable-linear integral pairing and unique holomorphic representatives (The Bergman space $A^{2} (Ω)$ and the Bergman kernel, $A^{2} (Ω)$ is closed, and the Bergman kernel is the sum over any complete orthonormal system).

[F2]

For a closed subspace $M$ of a Hilbert space, each $x$ has a unique decomposition $x = P_{M} x + (x - P_{M} x)$ with $P_{M} x \in M$ and $x - P_{M} x \in M^{⊥}$ ; $P_{M}$ is the Hilbert orthogonal projection and is the identity on $M$ (Orthogonal decomposition by a closed subspace, The Hilbert orthogonal projection onto a closed subspace).

[F3]

The Hilbert orthogonal projection is linear, self-adjoint and contractive (Hilbert projections are linear, self-adjoint and contractive).

[F4]

Evaluation at $w$ has unique Riesz representer $k_{w} \in A^{2} (Ω)$ , $f (w) = ⟨ f, k_{w} ⟩$ , and $K_{Ω} (z, w) = k_{w} (z)$ (The Bergman space $A^{2} (Ω)$ and the Bergman kernel).

[F5]

Cauchy–Schwarz gives $∣ ⟨ f, k_{w} ⟩ ∣ \leq ∥ f ∥_{2} ∥ k_{w} ∥_{2}$ , with equality exactly when the pair is linearly dependent (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs).

Proof

technique · direct, using the Riesz representation and orthogonal projection

Given: ${A C}_{ω}$ , a nonempty open $Ω \subseteq C^{m}$ , its Bergman space $A^{2} (Ω)$ , and $w \in Ω$ .

1.1A1F1F4given

By [F4], evaluation at $w$ is represented by $k_{w} = K_{Ω} (\cdot, w)$ , so for each $f \in A^{2} (Ω)$ , $f (w) = ⟨ f, k_{w} ⟩ = \int_{Ω} f (z) \overline{k_{w} (z)} d λ_{Ω} (z)$ . The definition $K_{Ω} (z, w) = k_{w} (z)$ gives the stated reproducing integral.

1.2A1F1F2F3given

By [F1], $A^{2} (Ω)$ is a closed subspace of $L^{2} (Ω)$ , so [F2] defines its unique orthogonal projection $P$ . The projection lemma [F3] gives linearity, self-adjointness and contractivity; [F2] also gives $P f = f$ for $f \in A^{2} (Ω)$ .

2.1A1F1F2F4step 1.1step 1.2given

For $f \in L^{2} (Ω)$ , [F2] gives $f - P f \in A^{2} (Ω)^{⊥}$ and $k_{w} \in A^{2} (Ω)$ by [F4]. Hence $⟨ f - P f, k_{w} ⟩ = 0$ . Applying step 1.1 to $P f \in A^{2} (Ω)$ and using linearity in the first variable, $P f (w) = ⟨ P f, k_{w} ⟩ = ⟨ f, k_{w} ⟩$ ; expanding $k_{w} (z)$ as $K_{Ω} (z, w)$ gives the displayed integral.

3.1A1F1F4F5step 1.1given∎

Applying step 1.1 to $k_{w}$ gives $K_{Ω} (w, w) = k_{w} (w) = ⟨ k_{w}, k_{w} ⟩ = ∥ k_{w} ∥_{2}^{2}$ . For any $f \in A^{2} (Ω)$ , [F4] and [F5] imply $∣ f (w) ∣^{2} \leq ∥ f ∥_{2}^{2} ∥ k_{w} ∥_{2}^{2}$ , so the supremum over the unit ball is at most $∥ k_{w} ∥_{2}^{2}$ . If $k_{w} \neq 0$ , the unit vector $k_{w} / ∥ k_{w} ∥_{2}$ attains this bound. Any other maximizer must give equality in [F5], hence is linearly dependent on $k_{w}$ ; its norm must be $1$ , so it is exactly $λ k_{w} / ∥ k_{w} ∥_{2}$ with $∣ λ ∣ = 1$ . If $k_{w} = 0$ , step 1.1 gives $f (w) = 0$ for every $f \in A^{2} (Ω)$ , so the supremum is $0$ and every function in the unit ball attains it.

Depends on

Used by

Dependency tree · two levels

62 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

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