CorollaryStatement: 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.

Strict convexity gives uniqueness of a minimiser

Statement

Let $K$ be a convex subset of a real vector space and let $I : K \to (- \infty, + \infty]$ be proper and strictly convex (Convex and strictly convex functionals on a convex subset of a real vector space, Proper, coercive and weakly lower semicontinuous extended-real functionals). If $u, v \in K$ both minimise $I$ on $K$ , then $u = v$ .

Facts & Assumptions

Given: A convex subset $K$ of a real vector space and a proper, strictly convex extended-real functional $I : K \to (- \infty, + \infty]$ (Convex and strictly convex functionals on a convex subset of a real vector space, Proper, coercive and weakly lower semicontinuous extended-real functionals); points $u, v \in K$ that both minimise $I$ on $K$ , in the sense that $I (u) = I (v) = \inf_{K} I$ .

[F1]

Strict convexity: for $u \neq v$ with $I (u), I (v) < + \infty$ and $λ \in (0, 1)$ one has $I (λ u + (1 - λ) v) < λ I (u) + (1 - λ) I (v)$ ; convexity gives $λ u + (1 - λ) v \in K$ (Convex and strictly convex functionals on a convex subset of a real vector space).

[F2]

The infimum is a lower bound: $\inf_{K} I \leq I (w)$ for every $w \in K$ (Greatest lower bound (infimum)).

Proof

technique · direct, by evaluating strict convexity at the midpoint of two minimisers

1.1F1F2given

Set-up. Let $u, v \in K$ both minimise $I$ and suppose for contradiction that $u \neq v$ . Properness gives $\inf_{K} I < + \infty$ , so $t : = \inf_{K} I = I (u) = I (v)$ is finite.

2.1F1step 1.1algebra

Strict convexity at the midpoint. The midpoint $w : = \frac{1}{2} u + \frac{1}{2} v$ lies in the convex set $K$ , and strict convexity with $λ = \frac{1}{2}$ applies because $u \neq v$ and $I (u) = I (v) = t < + \infty$ : hence $I (w) < \frac{1}{2} I (u) + \frac{1}{2} I (v) = t$ .

3.1F2step 2.1∎

Contradiction. Step 2.1 gives $I (w) < t = \inf_{K} I$ , while [F2] gives $\inf_{K} I \leq I (w)$ since $w \in K$ . This is impossible, so $u = v$ ; two distinct minimisers cannot exist.

Remarks

Properness is necessary. Without it the statement is false: on $K = [0, 1] \subseteq R$ the functional $I \equiv + \infty$ is convex and vacuously strictly convex, and $0$ and $1$ are two distinct points at which $I$ equals $\inf_{K} I = + \infty$ . Properness, equivalently the existence of a finite competitor, is what excludes this degenerate case, and it holds in the finite-valued integral-functional applications (Proper, coercive and weakly lower semicontinuous extended-real functionals).

Depends on

Used by

Dependency tree · two levels

10 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)
Riccardo Cristoferi, Calculus of Variations: Lecture Notes, Carnegie Mellon University 2016 (complete 133-page notes) (standard reference, not scraped)