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

A Hopf--Lax minimiser satisfies the characteristic Euler relation at differentiability points

Statement

Let $H : R^{n} \to R$ be convex and superlinear with Legendre transform $L$ , let $u_{0} : R^{n} \to R$ be bounded and continuous, and let $t > 0$ , $x \in R^{n}$ . Let $y$ be a minimiser of $φ (y) : = u_{0} (y) + t L ((x - y) / t)$ , which exists by Finiteness, superlinearity of the Lagrangian and localisation of Hopf--Lax near-minimisers, put $v : = (x - y) / t$ , and set $u : = Q_{t} u_{0}$ . Then: (1) if $u_{0}$ is differentiable at $y$ and $L$ is differentiable at $v$ , then $D u_{0} (y) = D L (v)$ ; (2) if $L$ is differentiable at $v$ and $u$ is differentiable at $x$ , then $D u (x) = D L (v)$ . No choice principle is used.

Facts & Assumptions

Given: A convex superlinear $H$ with Legendre transform $L$ , bounded continuous $u_{0}$ , $t > 0$ , $x \in R^{n}$ , a minimiser $y$ of $φ (y) = u_{0} (y) + t L ((x - y) / t)$ , $v = (x - y) / t$ , $u = Q_{t} u_{0}$ , and the Euclidean norm $∣ \cdot ∣$ .

[F1]

$Q_{t} u_{0} (x) = \inf_{y \in R^{n}} {u_{0} (y) + t L ((x - y) / t)}$ , and the infimum is attained under the present hypotheses (The Hopf--Lax operator and the Hopf--Lax formula, Finiteness, superlinearity of the Lagrangian and localisation of Hopf--Lax near-minimisers).

[F2]

$f$ is differentiable at $a$ with derivative $D f (a)$ exactly when $f (a + h) = f (a) + D f (a) h + r (h)$ with $r (h) / ∣ h ∣ \to 0$ as $h \to 0$ ; in that case every directional derivative exists and equals $D f (a) h$ (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ).

Proof

technique · expand the minimality inequality to first order in the direction of the perturbation

1.1F1F2algebra

First-order condition at a minimiser. Fix $h \in R^{n}$ and $τ \in (0, 1)$ ; minimality of $y$ at the point $x$ gives $u_{0} (y) + t L (v) \leq u_{0} (y + τ h) + t L (v - τ h / t)$ , where $u_{0} (y) + t L (v) = Q_{t} u_{0} (x)$ by [F1]. Assume $u_{0}$ is differentiable at $y$ and $L$ at $v$ . Then $u_{0} (y + τ h) = u_{0} (y) + τ ⟨ D u_{0} (y), h ⟩ + r_{u} (τ h)$ and $L (v - τ h / t) = L (v) - τ ⟨ D L (v), h / t ⟩ + r_{L} (- τ h / t)$ with $r_{u} (τ h) / ∣ τ h ∣ \to 0$ and $r_{L} (- τ h / t) / ∣ τ h ∣ \to 0$ as $τ ↓ 0$ by [F2]. Substituting and cancelling $u_{0} (y) + t L (v)$ gives $τ ⟨ D u_{0} (y), h ⟩ + r_{u} (τ h) \geq τ ⟨ D L (v), h ⟩ - t r_{L} (- τ h / t)$ ; dividing by $τ > 0$ and letting $τ ↓ 0$ gives $⟨ D u_{0} (y), h ⟩ \geq ⟨ D L (v), h ⟩$ .

2.1step 1.1F2algebra∎

The two equalities. The inequality of step 1.1 holds for every $h \in R^{n}$ ; applying it to $- h$ as well gives $⟨ D u_{0} (y) - D L (v), h ⟩ \geq 0$ and $⟨ D u_{0} (y) - D L (v), - h ⟩ \geq 0$ , that is $∣ ⟨ D u_{0} (y) - D L (v), h ⟩ ∣ \leq 0$ for all $h$ . Taking $h = D u_{0} (y) - D L (v)$ gives $∣ D u_{0} (y) - D L (v) ∣^{2} \leq 0$ , hence $D u_{0} (y) = D L (v)$ , which is (1). For (2), minimality of $y$ at the point $x + τ h$ gives $u (x + τ h) = Q_{t} u_{0} (x + τ h) \leq u_{0} (y) + t L (v + τ h / t) = u (x) + t (L (v + τ h / t) - L (v))$ , and if $L$ is differentiable at $v$ and $u$ at $x$ then [F2] gives $u (x + τ h) = u (x) + τ ⟨ D u (x), h ⟩ + r_{1} (τ h)$ and $t (L (v + τ h / t) - L (v)) = τ ⟨ D L (v), h ⟩ + r_{2} (τ h)$ with $r_{i} (τ h) / (τ ∣ h ∣) \to 0$ . Dividing by $τ$ and letting $τ ↓ 0$ gives $⟨ D u (x), h ⟩ \leq ⟨ D L (v), h ⟩$ for every $h$ ; applying this to $- h$ yields $D u (x) = D L (v)$ by the same argument as above, which is (2).

Remarks

Differentiability is assumed only where used. The minimiser exists by the localisation lemma, and the first-order conditions are obtained by perturbing the minimiser in a direction and expanding: no global smoothness of $u_{0}$ , $L$ or $Q_{t} u_{0}$ is asserted, and in the convex-quadratic case $H (p) = ∣ p ∣^{2} / 2$ a minimiser need not be unique when $u_{0}$ is merely continuous.
Direction of the two relations. Part (1) relates the datum to the Lagrangian at the minimiser, part (2) relates the value function to the Lagrangian at the same minimiser; together they identify the slope of the minimising chord with the conjugate momentum.

Depends on

Used by

The quadratic Hopf--Lax formula as an infimal convolution Example

Dependency tree · two levels

23 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

Hung Vinh Tran, Hamilton--Jacobi Equations: Theory and Applications, 2020 preliminary author manuscript of AMS Graduate Studies in Mathematics 213 (complete text) (standard reference, not scraped)