LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-30

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 lower semicontinuity of the Sobolev norm

Statement

Assume the Axiom of Choice. Let $Ω \subseteq R^{n}$ be open, $n \geq 1$ , $k \in N_{0}$ , $1 < p < \infty$ , and $K \in {R, C}$ . If a sequence $(u_{j})$ in $W^{k, p} (Ω; K)$ converges weakly to $u \in W^{k, p} (Ω; K)$ with respect to the displayed norm of Integer-order Sobolev spaces and their norms, then $∥ u ∥_{W^{k, p} (Ω)} \leq {lim inf}_{j \to \infty} ∥ u_{j} ∥_{W^{k, p} (Ω)} .$

The statement uses the exact norm convention of the Sobolev definition: the finite $ℓ^{p}$ sum of derivative norms for $1 \leq p < \infty$ and the maximum for $p = \infty$ . Neither reflexivity nor completeness of the space is used; the exponent hypothesis $1 < p < \infty$ is retained from the intended use, and the argument would apply to every $1 \leq p \leq \infty$ . If $Ω = \emptyset$ , then the space is the zero space and both sides are $0$ .

Facts & Assumptions

Given: AC, open $Ω \subseteq R^{n}$ , $k \in N_{0}$ , $1 < p < \infty$ , $K \in {R, C}$ , and a sequence $u_{j} ⇀ u$ in $W^{k, p} (Ω; K)$ .

[F1]

HB is the real dominated-extension principle: every real linear functional on a subspace dominated by a sublinear functional extends to the whole space with the same domination (The real dominated-extension principle as an additional hypothesis over ZF).

[F2]

Under the Axiom of Choice the dominated-extension theorem holds for every real vector space, sublinear functional and dominated linear functional, which is precisely the assertion HB (Hahn-Banach dominated extension theorem for real vector spaces).

[F3]

Under HB, if a net $x_{i}$ converges weakly to $x$ in a real or complex normed space $X$ , then $∥ x ∥ \leq {lim inf}_{i} ∥ x_{i} ∥$ , with no boundedness or completeness hypothesis (Weak convergence implies lower semicontinuity of the norm).

[F4]

Weak convergence of a sequence in a normed space means convergence against every bounded linear functional (Weak convergence of nets and sequences).

[F5]

Assuming Countable Choice, for either scalar field and all $k \in N_{0}$ , $1 \leq p \leq \infty$ , the displayed $W^{k, p} (Ω)$ formula is finite, vanishes exactly on the zero class, and makes $W^{k, p} (Ω; K)$ a normed space with the same derivative classes as Integer-order Sobolev spaces and their norms (The Sobolev norm descends to equivalence classes, Integer-order Sobolev spaces and their norms).

[F6]

The Axiom of Choice is the assertion that every family of nonempty sets has a choice function (The Axiom of Choice). In particular, applying it to families indexed by $N$ gives Countable Choice.

Proof

technique · obtain HB from AC, recognise the Sobolev space as a normed space under the displayed norm, and invoke the published dual-norming lower-semicontinuity corollary

1.1F1F2F6given

By [F6], the Axiom of Choice is available, so [F2] gives the real dominated-extension theorem; comparing its conclusion with the definition [F1] shows that HB holds.

1.2F4F5F6given

By [F6], AC supplies the Countable Choice hypothesis of [F5]. By [F5] the set $W^{k, p} (Ω; K)$ with the displayed formula is a normed space over $K$ , for both $K = R$ and $K = C$ , and $u_{j}, u$ are points of it. The weak convergence in the statement is convergence against every bounded linear functional of this normed space, as recalled in [F4], so $(u_{j})$ is a net in the sense required by [F3].

2.1F3step 1.1step 1.2

Apply [F3] with $X = W^{k, p} (Ω; K)$ , $x_{j} = u_{j}$ and $x = u$ . Its hypothesis is exactly the weak convergence of step 1.2, and its conclusion is $∥ u ∥ \leq {lim inf}_{j} ∥ u_{j} ∥$ , which is the displayed Sobolev-norm inequality. No reflexivity, uniform convexity, boundedness of the sequence, or completeness of $X$ is used in this application.

3.1F1F2F3F5F6step 1.1step 1.2step 2.1

The choice accounting and boundary cases are explicit. The Axiom of Choice supplies HB in step 1.1 through [F2] and Countable Choice in step 1.2 through [F6] for the Sobolev definition and norm theorem [F5]. The abstract lower-semicontinuity corollary [F3] needs HB, and the Sobolev normed-space interface retains its Countable Choice hypothesis; neither use is asserted to be choice-free. The exponent hypothesis $1 < p < \infty$ and the differentiability order $k$ enter only through the normed-space structure of $W^{k, p}$ , so the same argument covers $p = 1$ and $p = \infty$ ; they are recorded as a hypothesis rather than used. If $Ω = \emptyset$ , then by [F5] the space is the zero space, its norm is zero, and the inequality reads $0 \leq {lim inf}_{j} 0 = 0$ . If the sequence is the zero sequence or a constant sequence, both sides equal the common norm. $□$

Sources

Juha Kinnunen, Sobolev Spaces, §§1.1–1.4, 2.2, 2.6, 3.1–3.5: weak convergence in $W^{k, p}$ and the lower semicontinuity of the norm under weak limits.
John K. Hunter, Notes on Partial Differential Equations, Chapter 3 §§3.1–3.5: the same use of weak compactness and norm lower semicontinuity for Sobolev spaces.
The functional-analytic input is the published pair The real dominated-extension principle as an additional hypothesis over ZF / Weak convergence implies lower semicontinuity of the norm: the corollary assumes HB, which the Axiom of Choice supplies through Hahn-Banach dominated extension theorem for real vector spaces.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

28 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

Juha Kinnunen, Sobolev Spaces (Aalto University, 2026) (standard reference, not scraped)
John K. Hunter, Notes on Partial Differential Equations (2014) (standard reference, not scraped)