LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)

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.

The real zero-mean $L^{2}$ space is Hilbert

Statement

Assume Countable Choice. Let $D \subset R^{d}$ be a measurable set of finite measure, and set $L_{0}^{2} (D) : = {q \in L^{2} (D; R) : \int_{D} q d x = 0} .$ With the real $L^{2}$ inner product $(q, r) = \int_{D} q r d x$ , $L_{0}^{2} (D)$ is a closed real Hilbert subspace of $L^{2} (D; R)$ .

Facts & Assumptions

Given: Countable Choice, a finite-measure set $D$ , and the real Hilbert space $L^{2} (D; R)$ with its integral inner product.

[A1]

The published real $L^{2}$ Hilbert-space result assumes Countable Choice. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F1]

The integral inner product is well-defined, induces the quotient $L^{2}$ norm, and makes real $L^{2} (D)$ complete. ( $L^{2}$ with the integral pairing is a Hilbert space)

[F2]

Holder's inequality gives $∣ \int_{D} q d x ∣ \leq ∣ D ∣^{1 / 2} ∥ q ∥_{2}$ for $q \in L^{2} (D)$ . (Holder's inequality for integrals, including the endpoint cases)

[F3]

A closed linear subspace of a Banach space is complete with the inherited norm. (A closed subspace of a Banach space is Banach)

Proof

1.1F2given

Define $ℓ (q) : = \int_{D} q d x$ . By [F2], $∣ ℓ (q) ∣ \leq ∣ D ∣^{1 / 2} ∥ q ∥_{2}$ , and linearity of the integral makes $ℓ$ a bounded real linear functional. Its kernel is exactly $L_{0}^{2} (D)$ .

2.1step 1.1algebra

The kernel of a continuous functional is closed: if $q_{n} \in L_{0}^{2} (D)$ and $q_{n} \to q$ in $L^{2}$ , then $∣ ℓ (q) ∣ = ∣ ℓ (q - q_{n}) ∣ \leq ∣ D ∣^{1 / 2} ∥ q - q_{n} ∥_{2} \to 0$ , so $ℓ (q) = 0$ . Thus $L_{0}^{2} (D)$ is a closed linear subspace of $L^{2} (D)$ .

3.1A1F1F3step 2.1∎

The inner product on $L^{2} (D)$ restricts to an inner product on $L_{0}^{2} (D)$ and induces the inherited $L^{2}$ norm. By [F1], $L^{2} (D)$ is complete; by [F3] and step 2.1, its closed subspace $L_{0}^{2} (D)$ is complete. Therefore it is a real Hilbert space with the restricted inner product.

Depends on

Used by

No-flow mixed Darcy problem and coefficient norms Definition
Continuous mixed Darcy well-posedness with pressure gauge Theorem

Dependency tree · two levels

32 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

Jean-Luc Guermond, MATH 661 Fall 2025, Part XI Chapter 49: Well-posedness for PDEs in mixed form (standard reference, not scraped)
Daniele Boffi, Franco Brezzi and Michel Fortin, Mixed Finite Element Methods and Applications (standard reference, not scraped)

The real zero-mean L2L2 space is Hilbert