LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

Weak H^1 convergence plus Rellich preserves the L^2 unit normalisation

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $n \geq 1$ , let $Ω \subseteq R^{n}$ be a bounded open set, and let $(u_{j}) \subseteq H_{0}^{1} (Ω)$ be norm bounded with $u_{j} ⇀ u$ weakly in $H_{0}^{1} (Ω)$ (Weak convergence of nets and sequences, Zero-boundary Sobolev space as a norm closure, Integer-order Sobolev spaces and their norms) and $∥ u_{j} ∥_{L^{2} (Ω)} = 1$ for every $j$ (The space $L^{p} (μ)$ as the quotient by null functions). Then $u \in H_{0}^{1} (Ω)$ , $∥ u ∥_{L^{2} (Ω)} = 1$ , and some subsequence $(u_{j_{k}})$ converges to $u$ in $L^{2} (Ω)$ .

Facts & Assumptions

Given: A bounded open set $Ω \subseteq R^{n}$ , a norm-bounded sequence $(u_{j})$ in $H_{0}^{1} (Ω) = W_{0}^{1, 2} (Ω)$ converging weakly to $u$ , with $∥ u_{j} ∥_{L^{2} (Ω)} = 1$ for every $j$ , and the Axiom of Choice.

[A1]

AC implies DC implies countable choice, The Axiom of Choice, The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain, The Axiom of Countable Choice ( ${A C}_{ω}$ ): the Axiom of Choice implies Dependent Choice, which implies Countable Choice, so every Countable-Choice hypothesis below is discharged.

[F1]

Compactness of $W_{0}^{1, p} (Ω) ↪ L^{p} (Ω)$ on bounded open sets: for a bounded open $Ω \subseteq R^{n}$ and $1 \leq p < \infty$ the inclusion $W_{0}^{1, p} (Ω) \to L^{p} (Ω)$ is compact: every sequence bounded in $W_{0}^{1, p} (Ω)$ has a subsequence converging in $L^{p} (Ω)$ .

[F2]

Integer-order Sobolev spaces and their norms, Zero-boundary Sobolev space as a norm closure: the $W^{1, 2}$ norm dominates the $L^{2}$ norm, so $∥ v ∥_{L^{2} (Ω)} \leq ∥ v ∥_{W_{0}^{1, 2} (Ω)}$ for every $v \in H_{0}^{1} (Ω)$ , and $H_{0}^{1} (Ω) = W_{0}^{1, 2} (Ω)$ is a closed subspace of $W^{1, 2} (Ω)$ contained in $L^{2} (Ω)$ .

[F3]

Weak convergence of nets and sequences: $u_{j} ⇀ u$ in $H_{0}^{1} (Ω)$ means $f (u_{j}) \to f (u)$ for every bounded linear functional $f$ on $H_{0}^{1} (Ω)$ ; in particular the specified limit $u$ lies in $H_{0}^{1} (Ω)$ , and every subsequence inherits the convergence to the same limit.

[F4]

Holder's inequality for integrals, including the endpoint cases: applying real Hölder to $∣ v ∣$ and $∣ w ∣$ gives $\int_{Ω} ∣ v w ∣ \leq ∥ v ∥_{L^{2}} ∥ w ∥_{L^{2}}$ for real or complex $v, w \in L^{2} (Ω)$ .

[F5]

A function with nonnegative test pairings is nonnegative a.e.: under Countable Choice, if $ζ \in L^{2} (O; R)$ and $\int_{O} ζ φ = 0$ for every $φ \in C_{c}^{\infty} (O)$ , then $ζ = 0$ a.e. on $O$ (second clause of that lemma).

[F6]

The reverse triangle inequality in a normed space: $∣ ∥ a ∥ - ∥ b ∥ ∣ \leq ∥ a - b ∥$ in a normed space.

[F7]

The space $L^{p} (μ)$ as the quotient by null functions: elements of $L^{2} (Ω)$ are a.e. classes, and equality of two classes means equality almost everywhere.

Proof

technique · direct

Given: A bounded open set $Ω \subseteq R^{n}$ , a norm-bounded sequence $(u_{j})$ in $H_{0}^{1} (Ω)$ with $u_{j} ⇀ u$ and $∥ u_{j} ∥_{L^{2}} = 1$ for all $j$ , and the Axiom of Choice.

1.1givenF1F2

By [F1] with $p = 2$ and the bounded open set $Ω$ , applied to the norm-bounded sequence $(u_{j}) \subseteq W_{0}^{1, 2} (Ω) = H_{0}^{1} (Ω)$ , there are a subsequence $(u_{j_{k}})$ and a class $w \in L^{2} (Ω)$ with $∥ u_{j_{k}} - w ∥_{L^{2} (Ω)} \to 0$ .

2.1step 1.1F2F3F4F5F7

We claim $w = u$ in $L^{2} (Ω)$ . Fix a real test $φ \in C_{c}^{\infty} (Ω; R)$ and consider the linear functional $f_{φ} (v) : = \int_{Ω} v φ$ , which is bounded on $H_{0}^{1} (Ω)$ because $∣ f_{φ} (v) ∣ \leq ∥ v ∥_{L^{2}} ∥ φ ∥_{L^{2}} \leq ∥ v ∥_{W^{1, 2}} ∥ φ ∥_{L^{2}}$ by [F2, F4]. Since $(u_{j_{k}})$ is a subsequence of a weakly convergent sequence, [F3] gives $f_{φ} (u_{j_{k}}) \to f_{φ} (u)$ , that is $\int_{Ω} u_{j_{k}} φ \to \int_{Ω} u φ$ ; on the other hand [F4] gives $∣ \int_{Ω} (u_{j_{k}} - w) φ ∣ \leq ∥ u_{j_{k}} - w ∥_{L^{2}} ∥ φ ∥_{L^{2}} \to 0$ , so $\int_{Ω} (u - w) φ = 0$ for every $φ \in C_{c}^{\infty} (Ω)$ . Writing $ζ : = u - w \in L^{2} (Ω)$ , the real and imaginary parts belong to $L^{2} (Ω; R)$ since their absolute values are at most $∣ ζ ∣$ . Their pairings with every real test vanish separately. The second clause of [F5], with both open sets equal to $Ω$ , therefore applies to each part: zero pairings in particular satisfy its nonnegative-pairing hypothesis. Both parts vanish a.e., so $ζ = 0$ a.e. and $w = u$ by [F7]; for real scalars the imaginary part is zero already.

3.1step 1.1step 2.1F6algebra

By step 1.1 and step 2.1 the subsequence converges to $u$ in $L^{2} (Ω)$ ; since $∥ u_{j_{k}} ∥_{L^{2}} = 1$ for every $k$ , the reverse triangle inequality [F6] gives $∣ ∥ u ∥_{L^{2}} - ∥ u_{j_{k}} ∥_{L^{2}} ∣ \leq ∥ u - u_{j_{k}} ∥_{L^{2}} \to 0$ , hence $∥ u ∥_{L^{2} (Ω)} = 1$ .

4.1step 1.1step 3.1A1F3∎

The weak limit $u$ lies in $H_{0}^{1} (Ω)$ by [F3]; the subsequence $(u_{j_{k}})$ converges to $u$ in $L^{2} (Ω)$ by steps 1.1 and 2.1; and $∥ u ∥_{L^{2} (Ω)} = 1$ by step 3.1. This proves the assertion; the Countable Choice required by [F5] and by the extraction in [F1] is supplied by the Axiom of Choice through [A1].

Depends on

Used by

Dependency tree · two levels

60 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

Gerald Teschl, Partial Differential Equations: From Classical to Modern (2026 author manuscript; complete 392-page archived text) (standard reference, not scraped)