LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

A convex norm-lower-semicontinuous functional is weakly lower semicontinuous

Statement

Assume HB (The real dominated-extension principle as an additional hypothesis over ZF) and Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $X$ be a real normed space, let $K \subseteq X$ be nonempty and convex (Convex and strictly convex functionals on a convex subset of a real vector space) and let $I : K \to (- \infty, + \infty]$ be convex and sequentially lower semicontinuous in the norm topology (Proper, coercive and weakly lower semicontinuous extended-real functionals). Then $I$ is weakly sequentially lower semicontinuous on $K$ : for every $(u_{j}) \subseteq K$ with $u_{j} ⇀ u \in K$ (Weak convergence of nets and sequences), $I (u) \leq {lim inf}_{j} I (u_{j}) .$

Facts & Assumptions

Given: HB and Countable Choice; a real normed space $X$ , a nonempty convex set $K \subseteq X$ , and a convex functional $I : K \to (- \infty, + \infty]$ that is sequentially lower semicontinuous in the norm topology.

[F1]

A convex functional has convex sublevel sets: for every $t \in R$ the set ${v \in K : I (v) \leq t}$ is convex (Convex and strictly convex functionals on a convex subset of a real vector space).

[F2]

Norm sequential lower semicontinuity means $I (v) \leq {lim inf}_{j} I (v_{j})$ whenever $v_{j} \to v \in K$ in norm with $v_{j} \in K$ (Proper, coercive and weakly lower semicontinuous extended-real functionals). It gives closedness of sublevels relative to $K$ , not necessarily in $X$ .

[F3]

Under HB the norm and weak closures in $X$ of any convex subset coincide (Norm closed convex iff weakly closed).

[F6]

Countable Choice selects a point from each nonempty set $S \cap B (u, 1 / m)$ , $m \geq 1$ , whenever $u$ lies in the norm closure of $S$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F4]

Weak convergence $u_{j} ⇀ u$ is convergence in $σ (X, X^{*})$ ; in particular every subsequence of a weakly convergent sequence converges weakly to the same limit (Weak convergence of nets and sequences).

[F5]

Limit inferior: if ${lim inf}_{j} a_{j} < t$ for a sequence in $(- \infty, + \infty]$ and a real $t$ , then $a_{j} \leq t$ for infinitely many $j$ , so a strictly increasing sequence of indices $j_{k}$ with $a_{j_{k}} \leq t$ for all $k$ exists (Limit superior and limit inferior of a real sequence as $\inf_{n} \sup_{k \geq n} x_{k}$ and $\sup_{n} \inf_{k \geq n} x_{k}$ in $\overline{R}$ ).

Proof

technique · direct, by comparing the norm and weak closures of a convex sublevel set

1.1F5givenalgebra

Suppose $u_{j} ⇀ u$ with $(u_{j}) \subseteq K$ and $u \in K$ , and put $ℓ : = {lim inf}_{j} I (u_{j})$ . If $I (u) > ℓ$ , then since $I (u) \in (- \infty, + \infty]$ there is a real $t$ with $ℓ < t < I (u)$ (if $I (u)$ is finite take $t$ between; if $I (u) = + \infty$ take any real $t > ℓ$ ).

2.1F4F5step 1.1

A subsequence in the sublevel set. By [F5], applied to the sequence $(I (u_{j}))$ and this $t$ , there is a strictly increasing sequence of indices $j_{k}$ with $I (u_{j_{k}}) \leq t$ for every $k$ . By [F4] the subsequence still satisfies $u_{j_{k}} ⇀ u$ .

3.1F1F3step 2.1

Use the ambient closures. Put $S_{t} : = {v \in K : I (v) \leq t}$ . It is nonempty by step 2.1 and convex by [F1]. Since $u_{j_{k}} \in S_{t}$ and $u_{j_{k}} ⇀ u$ , the point $u$ lies in the weak closure of $S_{t}$ in $X$ . By [F3] it therefore lies in its norm closure. No ambient closedness of $K$ or $S_{t}$ is required.

4.1F2F6step 3.1given

Recover the relative sublevel inequality. For each integer $m \geq 1$ , choose $v_{m} \in S_{t}$ with $∥ v_{m} - u ∥ < 1 / m$ , using [F6]. Then $v_{m} \to u$ in norm, $v_{m} \in K$ and $u \in K$ . Thus [F2] gives $I (u) \leq {lim inf}_{m} I (v_{m}) \leq t$ .

5.1step 4.1step 1.1∎

Conclusion. Step 4.1 gives $I (u) \leq t < I (u)$ by the choice of $t$ in step 1.1, a contradiction; hence $I (u) \leq ℓ = {lim inf}_{j} I (u_{j})$ . As $(u_{j})$ and $u$ were arbitrary, $I$ is weakly sequentially lower semicontinuous on $K$ .

Depends on

Used by

A nonconvex gradient energy can lose weak lower semicontinuity Counterexample
Higher eigenvalues by orthogonality-constrained minimisation Theorem
The direct method for convex integral functionals Theorem
The direct method in a reflexive Banach space Theorem
The first Dirichlet eigenfunction by constrained minimisation Theorem

Dependency tree · two levels

27 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)
Francesco Paolo Maiale (course by Giovanni Alberti), Lecture Notes Calculus of Variations A, University of Pisa (last update 21 August 2019; complete 149-page notes) (standard reference, not scraped)