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

Stationarity is sufficient for a global minimum of a convex differentiable functional

Statement

Let $K$ be a convex subset of a real Banach space and let $I : K \to (- \infty, + \infty]$ be convex (Convex and strictly convex functionals on a convex subset of a real vector space). Fix $u \in K$ with $I (u) < + \infty$ , and assume that for every $v \in K$ the finite one-sided admissible directional derivative $δ_{+} I (u; v - u) : = \lim_{t ↓ 0} \frac{I (u + t (v - u)) - I (u)}{t}$ exists and is nonnegative. Then $I (u) = \inf_{K} I$ . If $I$ is strictly convex, $u$ is the unique minimiser. In particular, for a real-valued Gateaux differentiable functional on an open neighbourhood of $K$ , the condition $δ I (u; v - u) \geq 0$ for every $v \in K$ suffices, since the one-sided derivative agrees with that of Gateaux and Frechet derivatives of a functional.

Facts & Assumptions

Given: A convex $K$ in a real Banach space; a convex extended-real functional $I$ ; a finite competitor $u \in K$ ; and finite nonnegative one-sided derivatives $δ_{+} I (u; v - u)$ for every $v \in K$ . Only $0 < t < 1$ is used, so the segment is admissible even when $u$ lies on the boundary of $K$ .

[F1]

Convexity of $I$ : for $w, z \in K$ and $λ \in [0, 1]$ one has $I (λ w + (1 - λ) z) \leq λ I (w) + (1 - λ) I (z)$ , with the extended-real conventions; in particular the segment ${u + ε (v - u) : ε \in [0, 1]}$ lies in $K$ for $v \in K$ (Convex and strictly convex functionals on a convex subset of a real vector space).

[F2]

Three-slope inequality: if $φ : I_{0} \to R$ is convex on an interval and $x < y < z$ lie in $I_{0}$ , then the secant slopes satisfy $s (x, y) \leq s (x, z) \leq s (y, z)$ , where $s (a, b) = (f (b) - f (a)) / (b - a)$ (For a convex function and $x < y < z$ , the three secant slopes satisfy $s (x, y) \leq s (x, z) \leq s (y, z)$ ). Equivalently, the supporting-line form of convexity applies at every interior point with a slope between the one-sided derivatives (Every slope between the left and right derivatives of a convex function gives a supporting line).

[F3]

The admissible derivative is the limit of the secant slopes $(φ_{w} (t) - φ_{w} (0)) / t$ as $t ↓ 0$ , where $φ_{w} (t) : = I (u + t w)$ . When an ordinary Gateaux derivative exists on an open neighbourhood, this is its one-sided restriction (Gateaux and Frechet derivatives of a functional).

[F4]

A proper, strictly convex functional has at most one minimiser on a convex set (Strict convexity gives uniqueness of a minimiser); in step 4.1 the functional is proper because $I (u)$ is finite.

Proof

technique · direct, by monotonicity of the secant slopes along the admissible segment

1.1F1F3given

Reduction to a segment. Fix $v \in K$ . If $I (v) = + \infty$ then $I (u) \leq I (v)$ is automatic because $I (u)$ is finite by hypothesis; so assume $I (v) < + \infty$ . Define $φ (ε) : = I (u + ε (v - u))$ for $ε \in [0, 1]$ . By [F1] the segment lies in $K$ and $φ (ε) \leq (1 - ε) I (u) + ε I (v) < + \infty$ , while $φ (ε) > - \infty$ by the codomain of $I$ ; hence $φ : [0, 1] \to R$ is a finite convex function.

1.2F3given

The one-sided derivative. By the differentiability hypothesis the secant slope $s (0, ε) = ε^{- 1} (φ (ε) - φ (0))$ has the finite limit $δ_{+} I (u; v - u) \geq 0$ as $ε ↓ 0$ .

2.1F2step 1.1

Secant comparison. By [F2], applied on the interval $[0, 1]$ to the convex function $φ$ and the points $0 < ε < 1$ , one has $s (0, ε) \leq s (0, 1)$ .

3.1step 1.2step 2.1algebra

Passing to the limit. Letting $ε ↓ 0$ in the inequality of step 2.1 gives $δ_{+} I (u; v - u) \leq s (0, 1) = φ (1) - φ (0) = I (v) - I (u)$ ; since $δ_{+} I (u; v - u) \geq 0$ by hypothesis, it follows that $I (v) \geq I (u)$ .

4.1F4step 3.1∎

Conclusion and uniqueness. As $v \in K$ was arbitrary, $I (u) \leq I (v)$ for every $v \in K$ , so $I (u)$ is a lower bound for $I$ on $K$ ; since $u \in K$ , it is the greatest lower bound, $I (u) = \inf_{K} I$ . If $I$ is moreover strictly convex and $v \in K$ is any other minimiser, then both $u$ and $v$ are finite minimisers and [F4] gives $u = v$ , so $u$ is the unique minimiser.

Depends on

Used by

Dependency tree · two levels

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