LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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 Sobolev space $H^{1}$ is a Hilbert space

Statement

Assume Countable Choice. Let $Ω \subseteq R^{n}$ be open, $n \geq 1$ , and $K \in {R, C}$ . On $H^{1} (Ω) = W^{1, 2} (Ω; K)$ (Integer-order Sobolev spaces and their norms, The notation $H^{k}$ and the reserved zero-boundary symbol) define $(u, v)_{H^{1}} : = (u, v)_{L^{2}} + \sum_{i = 1}^{n} (D_{i} u, D_{i} v)_{L^{2}},$ with the $L^{2}$ inner product of $L^{2}$ with the integral pairing is a Hilbert space. Then $(\cdot, \cdot)_{H^{1}}$ is an inner product on the Sobolev classes whose induced norm is the $W^{1, 2}$ norm of Integer-order Sobolev spaces and their norms, and $H^{1} (Ω)$ is a Hilbert space for it. The zero-boundary space $H_{0}^{1} (Ω)$ is a closed subspace of $H^{1} (Ω)$ (Zero-boundary Sobolev space as a norm closure) and hence a Hilbert space for the restricted inner product. The pairing is linear in the first argument and conjugate-linear in the second, in the convention of Real and complex inner-product spaces and their induced length.

Facts & Assumptions

Given: Countable Choice; an open $Ω \subseteq R^{n}$ , $n \geq 1$ ; a field $K \in {R, C}$ ; the space $H^{1} (Ω) = W^{1, 2} (Ω; K)$ with index set $A_{1} = {α \in N_{0}^{n} : ∣ α ∣ \leq 1} = {0, e_{1}, \dots, e_{n}}$ and the pairing $(u, v)_{H^{1}} : = (u, v)_{L^{2}} + \sum_{i = 1}^{n} (D_{i} u, D_{i} v)_{L^{2}}$ .

[F1]

Sobolev structure: each $D^{α} u$ is a well-defined $L^{2}$ class and the $W^{1, 2}$ norm is $∥ u ∥_{W^{1, 2}} = (\sum_{α \in A_{1}} ∥ D^{α} u ∥_{L^{2}}^{2})^{1 / 2}$ ; $H^{1} (Ω) = W^{1, 2} (Ω; K)$ by notation (Integer-order Sobolev spaces and their norms, The notation $H^{k}$ and the reserved zero-boundary symbol, The Sobolev norm descends to equivalence classes, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F2]

$L^{2}$ is a Hilbert space for the integral pairing: on real $L^{2}$ the pairing $\int f g$ and on complex $L^{2}$ the pairing $\int f \overline{g}$ are well-defined inner products with $⟨ f, f ⟩ = ∥ f ∥_{2}^{2}$ , complete for the quotient $L^{2}$ norm ( $L^{2}$ with the integral pairing is a Hilbert space, The space $L^{p} (μ)$ as the quotient by null functions, The $L^{p}$ norm descends to the quotient and makes $L^{p}$ a normed space for $1 \leq p \leq \infty$ , Complex Lp classes and Euclidean test-function conventions).

[F3]

An inner product is linear in the first argument, conjugate-symmetric, and positive definite; its induced length is a norm, and a Hilbert space is an inner-product space complete for that norm (Real and complex inner product spaces, with the inner product linear in the first argument, Real and complex inner-product spaces and their induced length, The induced length is a norm, Hilbert space).

[F4]

H"older: for $L^{2}$ classes $f, g$ , $∣ \int f \overline{g} ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ , with the real form $∣ \int f g ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ (Complex Holder, Minkowski, and the quotient norm, Holder's inequality for integrals, including the endpoint cases).

[F5]

$C_{c}^{\infty} (Ω; K)$ is a $K$ -vector space of test functions, and $H_{0}^{1} (Ω)$ is its closure in $H^{1}$ : explicitly, $u \in H_{0}^{1} (Ω)$ if and only if for every $δ > 0$ there is a test function $φ$ with $∥ u - φ ∥_{W^{1, 2}} < δ$ . A closure is closed and is the smallest closed superset (Complex Lp classes and Euclidean test-function conventions, Zero-boundary Sobolev space as a norm closure, The closure of a nonempty $A$ is ${x : d (x, A) = 0}$ , equals $A$ together with its limit points, and is the smallest closed superset).

[F6]

A closed linear subspace of a Banach space, with the restricted norm, is a Banach space (A closed subspace of a Banach space is Banach).

Proof

1.1F1F2F3

The pairing is a well-defined inner product: each summand $(D^{α} u, D^{α} v)_{L^{2}}$ is the $L^{2}$ pairing of the well-defined classes $D^{α} u$ and $D^{α} v$ , hence representative-independent; each is linear in the first argument and conjugate-linear in the second over $K$ , and conjugate-symmetric. A finite sum of maps with these properties again has them, so $(u, v)_{H^{1}}$ is well defined on classes, linear in $u$ , conjugate-linear in $v$ and conjugate-symmetric. It is positive definite, since $(u, u)_{H^{1}} = \sum_{α \in A_{1}} ∥ D^{α} u ∥_{L^{2}}^{2} \geq 0$ equals $0$ only when every $D^{α} u = 0$ , in particular $u = D^{0} u = 0$ , while $u = 0$ plainly gives $0$ .

1.2F5algebra

$H_{0}^{1} (Ω)$ is a linear subspace. It contains the zero class, as the zero test function shows. Let $u, v \in H_{0}^{1} (Ω)$ and $a, b \in K$ , and let $δ > 0$ . Using the test-function approximation of [F5], choose test functions $φ, ψ$ with $∥ u - φ ∥_{W^{1, 2}} < δ / (2 (∣ a ∣ + ∣ b ∣ + 1))$ and $∥ v - ψ ∥_{W^{1, 2}} < δ / (2 (∣ a ∣ + ∣ b ∣ + 1))$ ; then $a φ + b ψ$ is again a test function, and $∥ (a u + b v) - (a φ + b ψ) ∥_{W^{1, 2}} \leq ∣ a ∣ ∥ u - φ ∥_{W^{1, 2}} + ∣ b ∣ ∥ v - ψ ∥_{W^{1, 2}} < δ$ . So $a u + b v \in H_{0}^{1} (Ω)$ ; the space is a subspace and, being a closure, it is closed in $H^{1} (Ω)$ .

2.1F1F2step 1.1algebra

Its induced norm is the Sobolev norm: $(u, u)_{H^{1}} = \sum_{α \in A_{1}} ∥ D^{α} u ∥_{L^{2}}^{2} = ∥ u ∥_{W^{1, 2}}^{2}$ , so the induced length is $∥ u ∥_{W^{1, 2}}$ .

3.1F1F2F4step 2.1

Completeness: let $(u_{m})$ be a Cauchy sequence in $H^{1}$ . For each $α \in A_{1}$ the inequality $∥ D^{α} u_{m} - D^{α} u_{l} ∥_{L^{2}} \leq ∥ u_{m} - u_{l} ∥_{W^{1, 2}}$ shows that $(D^{α} u_{m})_{m}$ is Cauchy in $L^{2}$ , so it has a limit class $f_{α}$ . Fix $i$ and a test function $φ$ . The weak-derivative identity gives $\int_{Ω} u_{m} D_{i} φ d x = - \int_{Ω} D_{i} u_{m} φ d x$ for every $m$ ; H"older's inequality makes both sides converge to $\int_{Ω} f_{0} D_{i} φ d x$ and $- \int_{Ω} f_{i} φ d x$ , respectively, where $f_{0}$ is the limit of the classes $u_{m} = D^{0} u_{m}$ . Hence $\int f_{0} D_{i} φ = - \int f_{i} φ$ for every test function $φ$ , so $f_{0} \in W^{1, 2} (Ω; K)$ with $D_{i} f_{0} = f_{i}$ , and $∥ u_{m} - f_{0} ∥_{W^{1, 2}}^{2} = \sum_{α \in A_{1}} ∥ D^{α} u_{m} - f_{α} ∥_{L^{2}}^{2} \to 0$ . Thus every Cauchy sequence in $H^{1}$ converges in $H^{1}$ : the space is complete in its Sobolev norm.

4.1F1F3step 1.1step 2.1step 3.1

Consequences for the pairing: by steps 1.1, 2.1 the pairing is an inner product inducing the Sobolev norm, and by step 3.1 the space is complete for that norm; therefore $H^{1} (Ω)$ is a Hilbert space over $K$ for the pairing.

5.1F3F5F6step 4.1step 1.2

$H_{0}^{1} (Ω)$ is a Hilbert space: it is a closed linear subspace of the Hilbert space $H^{1} (Ω)$ , hence complete for the restricted norm by [F6] applied to the underlying Banach space, and the restriction of the inner product is an inner product whose induced norm is the restriction of the Sobolev norm.

6.1step 4.1step 5.1∎

The pairing $(\cdot, \cdot)_{H^{1}}$ is therefore an inner product on $H^{1} (Ω)$ inducing the $W^{1, 2}$ norm, making $H^{1} (Ω)$ a Hilbert space, while $H_{0}^{1} (Ω)$ is a closed subspace and a Hilbert space for the restricted pairing; the pairing is linear in the first argument and conjugate-linear in the second, as required.

Depends on

Used by

A positive reaction term restores coercivity without Poincar'e Corollary
A sufficiently large shift is coercive Corollary
A large adverse zero-order term destroys Dirichlet coercivity Counterexample
The Neumann Poisson problem is not coercive on all of H¹ Counterexample
Closed sectorial form and its associated operator Definition
The shifted elliptic solution operator Definition
A nonsymmetric coercive elliptic form Example
Eigenbasis expansion in the form norm Lemma
Every H⁻¹ functional is an L² function plus a divergence Theorem
Existence and uniqueness for the weak Dirichlet Poisson problem Theorem
Lax--Milgram solvability for coercive divergence-form equations Theorem
The Dirichlet principle for the Poisson equation Theorem
The first positive Neumann eigenvalue has the mean-zero Rayleigh characterisation Theorem
Weak Neumann solvability on the mean-zero subspace Theorem

Dependency tree · two levels

88 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

John K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page two-quarter notes) (standard reference, not scraped)
Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (Springer Universitext, 2011, complete 614-page text) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (archived 2025 author manuscript) (standard reference, not scraped)

The Sobolev space H1H1 is a Hilbert space