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.

The liminf passage makes the weak limit a minimiser

Statement

Let $A \subseteq X$ and $I : A \to (- \infty, + \infty]$ be proper, and let $(u_{j}) \subseteq A$ be a minimising sequence with $u_{j} ⇀ u \in A$ (Weak convergence of nets and sequences). If $I$ is weakly sequentially lower semicontinuous at $u$ (Proper, coercive and weakly lower semicontinuous extended-real functionals), then $I (u) = \inf_{A} I$ , so $u$ is a minimiser of $I$ on $A$ .

Facts & Assumptions

Given: A set $A \subseteq X$ , a proper extended-real functional $I : A \to (- \infty, + \infty]$ (Proper, coercive and weakly lower semicontinuous extended-real functionals), a minimising sequence $(u_{j}) \subseteq A$ with $u_{j} ⇀ u$ and $u \in A$ , and weak sequential lower semicontinuity of $I$ at $u$ .

[F1]

Weak sequential lower semicontinuity of $I$ at $u$ means $I (u) \leq {lim inf}_{j} I (u_{j})$ for every sequence $(u_{j}) \subseteq A$ with $u_{j} ⇀ u$ (Proper, coercive and weakly lower semicontinuous extended-real functionals, 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}$ ).

[F2]

Infimum and limit inferior: $\inf_{A} I$ is the greatest lower bound of $I$ on $A$ in $[- \infty, + \infty]$ and $\inf_{A} I \leq I (w)$ for every $w \in A$ (Proper, coercive and weakly lower semicontinuous extended-real functionals).

[F3]

If a sequence of extended reals converges to a limit, its limit inferior equals that limit (Proper, coercive and weakly lower semicontinuous extended-real functionals).

Proof

technique · direct

1.1F3F2given

The limit inferior of the values. Since $(u_{j})$ is minimising, $I (u_{j}) \to \inf_{A} I$ ; by [F3] therefore ${lim inf}_{j} I (u_{j}) = \inf_{A} I$ .

2.1F1step 1.1

Lower semicontinuity. Applying [F1] to the sequence $(u_{j})$ , which lies in $A$ and converges weakly to $u \in A$ , gives $I (u) \leq {lim inf}_{j} I (u_{j}) = \inf_{A} I$ .

2.2F2step 1.1

The reverse inequality. Since $u \in A$ , the defining property of the infimum [F2] gives $\inf_{A} I \leq I (u)$ .

3.1step 2.1step 2.2given∎

Conclusion. If $\inf_{A} I = - \infty$ , step 2.1 would give $I (u) \leq - \infty$ , impossible because $I$ takes values in $(- \infty, + \infty]$ ; hence under the hypotheses this case cannot occur. Otherwise $\inf_{A} I$ is finite, and steps 2.1 and 2.2 combine to $I (u) = \inf_{A} I$ , so $u$ attains the infimum and is a minimiser.

Depends on

Used by

The direct method in a reflexive Banach space Theorem

Dependency tree · two levels

14 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)