LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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 twice differentiable local minimiser has nonnegative second variation

Statement

Let $X$ be a real Banach space, $U \subseteq X$ open, $F : U \to R$ of class $C^{2}$ (C k map between Banach spaces) and let $u \in U$ be a local minimiser of $F$ , meaning that there is $δ > 0$ such that $F (w) \geq F (u)$ whenever $w \in U$ and $∥ w - u ∥ < δ$ . Then for every $v \in X$ $D^{2} F (u) [v, v] \geq 0,$ where $D^{2} F (u) \in B (X, B (X, R))$ is the second Frechet derivative of $F$ at $u$ (Fréchet derivative between Banach spaces); that is, the second variation of $F$ at $u$ is nonnegative in every direction.

Facts & Assumptions

Given: A real Banach space $X$ , an open set $U \subseteq X$ , a map $F : U \to R$ of class $C^{2}$ , a local minimiser $u \in U$ of $F$ , and a direction $v \in X$ .

[F1]

By the stated definition of local minimality, there is $δ > 0$ with $F (w) \geq F (u)$ for every $w \in U$ with $∥ w - u ∥ < δ$ ; in the terminology of Local (relative) maximum and minimum of $f : A \to R$ at a point, the strict forms, and what it means for the point to be interior to $A$ , $0$ is then an interior local minimum of the one-variable function $ε \mapsto F (u + ε v)$ (Local (relative) maximum and minimum of $f : A \to R$ at a point, the strict forms, and what it means for the point to be interior to $A$ ).

[F2]

The Banach-space calculus of C k map between Banach spaces together with the chain rule of Chain sum product and composition rules for Banach derivatives gives that $φ (ε) : = F (u + ε v)$ , defined for $∣ ε ∣$ small, is of class $C^{2}$ with $φ^{'} (ε) = D F (u + ε v) v$ and $φ^{''} (ε) = D^{2} F (u + ε v) [v, v]$ ; in particular $φ^{'} (0) = D F (u) v$ and $φ^{''} (0) = D^{2} F (u) [v, v]$ , where $D^{2} F (u) \in B (X, B (X, R))$ is the second Frechet derivative (Fréchet derivative between Banach spaces).

[F3]

If a differentiable function on a real interval has an interior local extremum at a point, then its derivative vanishes there (Fermat's interior extremum theorem: if $f$ has a local extremum at a point $c$ interior to its domain and is differentiable at $c$ , then $f^{'} (c) = 0$ ).

[F4]

Taylor's formula with Lagrange remainder at order $1$ : if $φ$ has derivatives through order $2$ on $[0, h]$ , then for some $ξ \in (0, h)$ one has $φ (h) = φ (0) + φ^{'} (0) h + \frac{1}{2} φ^{''} (ξ) h^{2}$ (The Lagrange and Cauchy forms of Taylor's remainder).

Proof

technique · direct, by reduction to a one-variable function along a line

1.1F1algebra

Reduction to one variable. If $v = 0$ then $D^{2} F (u) [0, 0] = 0$ because $D^{2} F (u)$ is linear in each variable, so assume $v \neq 0$ . Since $U$ is open, there is $η > 0$ with $u + ε v \in U$ for $∣ ε ∣ < η$ , and by [F1] there is $δ > 0$ with $F (w) \geq F (u)$ for $∥ w - u ∥ < δ$ . For $∣ ε ∣ < \min (η, δ / ∥ v ∥)$ the point $u + ε v$ lies in $U$ and $∥ (u + ε v) - u ∥ = ∣ ε ∣ ∥ v ∥ < δ$ , so $φ (ε) \geq φ (0)$ : the point $0$ is an interior local minimum of $φ$ .

1.2F2

The derivatives of the reduced function. By [F2] the function $φ$ is of class $C^{2}$ near $0$ , its second derivative is continuous there, and $φ^{'} (0) = D F (u) v$ , $φ^{''} (0) = D^{2} F (u) [v, v]$ .

2.1F3step 1.2

Fermat's theorem. In the case $v \neq 0$ of step 1.1 the point $0$ lies in the interior of the interval on which $φ$ is defined and is an interior local minimum of the differentiable function $φ$ , so $φ^{'} (0) = 0$ by [F3]; combined with step 1.2 this gives $D F (u) v = 0$ .

3.1F4step 2.1algebra

Taylor expansion at order one. Let $h > 0$ be small enough that $φ$ is of class $C^{2}$ on $[0, h]$ and $φ (h) \geq φ (0)$ . By [F4] there is $ξ_{h} \in (0, h)$ with $φ (h) - φ (0) = φ^{'} (0) h + \frac{1}{2} φ^{''} (ξ_{h}) h^{2}$ , and $φ^{'} (0) = 0$ by step 2.1, so $φ (h) - φ (0) = \frac{1}{2} φ^{''} (ξ_{h}) h^{2}$ . Since $φ (h) - φ (0) \geq 0$ and $h^{2} > 0$ , it follows that $φ^{''} (ξ_{h}) \geq 0$ .

4.1step 3.1step 1.2step 1.1∎

Passage to the limit. As $h ↓ 0$ one has $ξ_{h} \to 0$ because $0 < ξ_{h} < h$ , and $φ^{''}$ is continuous at $0$ by step 1.2, so $φ^{''} (0) = \lim_{h ↓ 0} φ^{''} (ξ_{h}) \geq 0$ . In the case $v \neq 0$ , $φ^{''} (0) = D^{2} F (u) [v, v]$ by step 1.2 and hence $D^{2} F (u) [v, v] \geq 0$ ; the case $v = 0$ was settled in step 1.1. As $v$ was arbitrary, the second variation of $F$ at $u$ is nonnegative in every direction.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

34 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

Riccardo Cristoferi, Calculus of Variations: Lecture Notes, Carnegie Mellon University 2016 (complete 133-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)