CounterexampleConstruction: Literature-sourcedVerification: 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 coercive functional need not attain without weak lower semicontinuity

Statement refuted

Counterexample. Assume the Axiom of Choice (The Axiom of Choice). Let $H = ℓ^{2} (N, R)$ (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ ), let $e_{k}$ be the family that is $1$ at $k$ and $0$ elsewhere, and define $I : H \to R$ by $I (0) : = 1, I (u) : = ∥ u ∥^{2} (u \neq 0) .$ Then $I$ is proper and coercive (Proper, coercive and weakly lower semicontinuous extended-real functionals) and $\inf_{H} I = 0$ , but no point of $H$ minimises $I$ : the value $0$ is not attained, because only $u = 0$ gives $∥ u ∥^{2} = 0$ and $I (0) = 1$ . The functional is not weakly sequentially lower semicontinuous at $0$ : for $j \geq 1$ , $e_{j} / j ⇀ 0$ while $I (e_{j} / j) = 1 / j^{2} \to 0 < 1 = I (0)$ . Hence the weak lower semicontinuity hypothesis in The direct method in a reflexive Banach space cannot be replaced by coercivity alone, even in a reflexive space.

Facts & Assumptions

Given: The Axiom of Choice; the real Hilbert space $H = ℓ^{2} (N, R)$ (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ ), its coordinate vectors $e_{k}$ , namely the family that is $1$ at $k$ and $0$ elsewhere, and the functional $I : H \to R$ with $I (0) : = 1$ and $I (u) : = ∥ u ∥^{2}$ for $u \neq 0$ . The counting-measure dictionary $ℓ^{p}$ is the $L^{p}$ space of counting measure identifies $H$ with real $L^{2} (#)$ , which is reflexive (and thus Banach) by Reflexivity of Lp for one less p less infinity under Countable Choice, supplied here by AC; the series pairing is its inner product.

[F1]

Proper, coercive and weakly sequentially lower semicontinuous functionals are defined as in Proper, coercive and weakly lower semicontinuous extended-real functionals; a functional is proper when its effective domain is nonempty, equivalently when its infimum is less than $+ \infty$ (it may be $- \infty$ ).

[F2]

In the direct method, weak sequential lower semicontinuity is a hypothesis alongside coercivity; The direct method in a reflexive Banach space states all of its hypotheses explicitly, so a coercive proper functional on a reflexive space need not attain when that hypothesis fails.

[F3]

Each coordinate vector satisfies $e_{k} \in H$ and $∥ e_{k} ∥ = 1$ , and $e_{k} ⇀ 0$ : by the duality of $ℓ^{p}$ and $ℓ^{q}$ every bounded linear functional on $ℓ^{2}$ is $Λ (a) = \sum_{k} a_{k} b_{k}$ for a unique $b \in ℓ^{2}$ (Counting measure specializes the representation theorem to $ℓ^{p}$ and $ℓ^{q}$ ), so $Λ (e_{k}) = b_{k}$ , and $b_{k} \to 0$ because a square-summable family has small tails, that is, for every $ε > 0$ there is a finite $F$ with $\sum_{k \notin F} ∣ b_{k} ∣^{2} < ε$ (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ ), whence $∣ b_{k} ∣^{2} < ε$ for every $k$ beyond all elements of $F$ ; weak convergence means convergence against every bounded linear functional (Weak convergence of nets and sequences).

Counterexample

technique · direct computation of the values along the sequence $e_j/j$, $j\ge1$

1.1F1algebra

$I$ is proper. The effective domain of $I$ is all of $H$ , which is nonempty, and $I \geq 0$ with $I (e_{1} / j) = 1 / j^{2} \to 0$ as $j \to \infty$ , so $\inf_{H} I = 0 < + \infty$ ; by [F1] the functional is proper.

1.2F1algebra

$I$ is coercive. For $∥ u ∥ \geq 1$ one has $I (u) = ∥ u ∥^{2} \geq ∥ u ∥$ (and the value $I (0) = 1$ does not affect large norms). Given $M \in R$ , put $R : = \max {1, M + 1}$ ; then $∥ u ∥ \geq R$ implies $I (u) \geq ∥ u ∥ \geq M + 1 > M$ , so every sublevel set is bounded and $I$ is coercive by [F1].

1.3F1algebra

None of the values $0$ is attained. If $I (u) = 0$ then $u \neq 0$ and $∥ u ∥^{2} = 0$ , hence $u = 0$ , a contradiction; and $I (0) = 1 \neq 0$ . Since $\inf_{H} I = 0$ , the infimum is not attained.

1.4F3algebra

Failure of weak lower semicontinuity at $0$ . Let $u_{j} : = e_{j} / j$ for $j \geq 1$ . Then $∥ u_{j} ∥ = 1 / j \to 0$ by [F3], and for every bounded linear functional $Λ$ on $H$ one has $Λ (u_{j}) = Λ (e_{j}) / j \to 0$ by [F3]; hence $u_{j} ⇀ 0$ . On the other hand $u_{j} \neq 0$ gives $I (u_{j}) = ∥ u_{j} ∥^{2} = 1 / j^{2} \to 0 < 1 = I (0)$ . Hence $I (0) > {lim inf}_{j} I (u_{j})$ , and $I$ is not weakly sequentially lower semicontinuous at $0$ .

2.1F2step 1.3step 1.4∎

Conclusion. The functional is proper and coercive on the reflexive space $H$ , yet attains no minimum and fails weak lower semicontinuity; hence the weak lower semicontinuity hypothesis of [F2] cannot be dropped, and coercivity alone does not give attainment even in a reflexive space.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

51 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

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)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2026 author manuscript; complete 392-page archived text) (standard reference, not scraped)