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.

The first variation vanishes at an interior minimiser

Statement

Let $X$ be a real Banach space, $U \subseteq X$ open, $F : U \to R$ Gateaux differentiable at $u \in U$ (Gateaux and Frechet derivatives of a functional) and suppose $u$ is a local minimiser of $F$ : $F (u) \leq F (w)$ for all $w \in U$ with $∥ w - u ∥$ small (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$ ). Then $δ F (u; v) = 0 for every v \in X .$ More generally, if $V \subseteq X$ is a linear subspace and $F (u) \leq F (w)$ for all $w \in (u + V) \cap U$ with $∥ w - u ∥$ small, then $δ F (u; v) = 0$ for every $v \in V$ .

Facts & Assumptions

Given: A real Banach space $X$ , an open set $U \subseteq X$ , a map $F : U \to R$ that is Gateaux differentiable at $u \in U$ , and the assumption that $u$ is a local minimiser: $F (u) \leq F (w)$ for all $w \in U$ with $∥ w - u ∥$ small. For the general form, a linear subspace $V \subseteq X$ with $F (u) \leq F (w)$ for all $w \in (u + V) \cap U$ with $∥ w - u ∥$ small.

[F1]

Gateaux differentiability of $F$ at $u$ means that $δ F (u; v) = \lim_{ε \to 0, ε \neq 0} ε^{- 1} (F (u + ε v) - F (u))$ exists for every $v \in X$ and that $v \mapsto δ F (u; v)$ is a bounded linear functional; for each fixed $v$ the function $φ (ε) : = F (u + ε v)$ satisfies $φ^{'} (0) = δ F (u; v)$ (Gateaux and Frechet derivatives of a functional).

[F2]

The point $0$ is an interior local minimum of $φ$ when $φ (0) \leq φ (ε)$ for all $ε$ with $∣ ε ∣$ small, the one-variable notion 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$ (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$ ).

[F3]

If a function on a real interval is differentiable at an interior local extremum, 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$ ).

Proof

technique · direct, reducing to the one-variable Fermat theorem along each admissible line

1.1F1F2given

Reduction to one variable. Fix $v \in X$ . Since $U$ is open and $u \in U$ , there is $ε_{0} > 0$ with $u + ε v \in U$ for every $∣ ε ∣ < ε_{0}$ ; define $φ (ε) : = F (u + ε v)$ for those $ε$ . By [F1] $φ^{'} (0)$ exists and equals $δ F (u; v)$ . The local minimality of $u$ gives $ε_{1} \in (0, ε_{0}]$ with $F (u) \leq F (u + ε v)$ , that is $φ (0) \leq φ (ε)$ , whenever $∣ ε ∣ < ε_{1}$ ; in the terminology of [F2], $0$ is an interior local minimum of $φ$ .

2.1F3step 1.1

Fermat's theorem applied to $φ$ . The function $φ$ is differentiable at its interior point $0$ and has a local minimum there, so by [F3] $φ^{'} (0) = 0$ ; by step 1.1 this reads $δ F (u; v) = 0$ .

3.1F1step 2.1∎

The general admissible-affine form. Let $V \subseteq X$ be a linear subspace and suppose $F (u) \leq F (w)$ for all $w \in (u + V) \cap U$ with $∥ w - u ∥$ small. Fix $v \in V$ . For $∣ ε ∣$ small the point $u + ε v$ belongs to $(u + V) \cap U$ , because $V$ is a linear subspace and $U$ is open; the argument of steps 1.1 and 2.1 therefore applies verbatim to this $v$ and yields $δ F (u; v) = 0$ . As $v \in V$ was arbitrary, the first variation vanishes on the whole subspace $V$ .

Depends on

Used by

Dependency tree · two levels

17 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)
Viktor Grigoryan, Math 246B Partial Differential Equations, UCSB 2011 (complete 31-page course notes) (standard reference, not scraped)