ExampleConstruction: Literature-sourcedVerification: 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 quadratic Hopf--Lax formula as an infimal convolution

Example

Let $n \geq 1$ and $H (p) = \frac{1}{2} ∣ p ∣^{2}$ . Its Legendre transform is $L (v) = \frac{1}{2} ∣ v ∣^{2}$ . For every bounded uniformly continuous $u_{0} : R^{n} \to R$ , the Hopf--Lax operator of The Hopf--Lax operator and the Hopf--Lax formula is, for $t > 0$ , $Q_{t} u_{0} (x) = \inf_{y \in R^{n}} {u_{0} (y) + \frac{∣ x - y ∣^{2}}{2 t}},$ the infimal convolution with the quadratic kernel $q_{t} (z) = ∣ z ∣^{2} / (2 t)$ . The infimum is attained, and for every minimiser $y$ the Euler relation $D u_{0} (y) = (x - y) / t$ holds whenever $u_{0}$ is differentiable at $y$ (A Hopf--Lax minimiser satisfies the characteristic Euler relation at differentiability points). Separately, the quadratic datum $w_{0} (y) = \frac{1}{2} ∣ y ∣^{2}$ is unbounded and so is outside the datum class in The Hopf--Lax operator and the Hopf--Lax formula. Its algebraic infimal convolution $I_{t} (x) : = \inf_{y \in R^{n}} {\frac{1}{2} ∣ y ∣^{2} + \frac{∣ x - y ∣^{2}}{2 t}}$ has the unique minimiser $y = x / (1 + t)$ and value $I_{t} (x) = ∣ x ∣^{2} / (2 (1 + t))$ ; this separate calculation is the Moreau envelope of the quadratic function and does not apply the bounded-data Hopf--Lax theorem to $w_{0}$ .

Verification

Given: The Hamiltonian $H (p) = \frac{1}{2} ∣ p ∣^{2}$ on $R^{n}$ , its Legendre transform $L$ , a bounded uniformly continuous datum $u_{0}$ , the operators $Q_{t}$ of The Hopf--Lax operator and the Hopf--Lax formula, and the unbounded quadratic datum $w_{0} (y) = \frac{1}{2} ∣ y ∣^{2}$ .

[F1] $L (v) = \sup_{p \in R^{n}} (p \cdot v - H (p))$ , the supremum taken in $\overline{R}$ (The Legendre transform of a finite-valued convex Hamiltonian).

[F2] For $t > 0$ , $Q_{t} u_{0} (x) = \inf_{y} {u_{0} (y) + t L ((x - y) / t)}$ , and under convexity and superlinearity of $H$ the infimum is finite and attained for bounded uniformly continuous $u_{0}$ (The Hopf--Lax operator and the Hopf--Lax formula, Finiteness, superlinearity of the Lagrangian and localisation of Hopf--Lax near-minimisers).

[F3] At a minimiser $y$ of $u_{0} (y) + t L ((x - y) / t)$ , if $u_{0}$ is differentiable at $y$ and $L$ at $(x - y) / t$ , then $D u_{0} (y) = D L ((x - y) / t)$ (A Hopf--Lax minimiser satisfies the characteristic Euler relation at differentiability points).

Proof technique: compute the quadratic conjugate, use the in-class Hopf--Lax suppliers only for bounded uniformly continuous data, and evaluate the separate quadratic infimum by completing the square.

1.1F1algebra

The conjugate of the quadratic Hamiltonian. Fix $v \in R^{n}$ and complete the square: $p \cdot v - \frac{1}{2} ∣ p ∣^{2} = \frac{1}{2} ∣ v ∣^{2} - \frac{1}{2} ∣ p - v ∣^{2}$ , whose supremum over $p$ is attained at $p = v$ with value $\frac{1}{2} ∣ v ∣^{2}$ . Hence $L (v) = \frac{1}{2} ∣ v ∣^{2}$ by [F1]; in particular $L$ is finite, convex and superlinear.

2.1step 1.1F2F3algebra

The formula, attainment and the Euler relation. Substituting $L (v) = ∣ v ∣^{2} / 2$ into the definition of $Q_{t}$ gives the displayed infimal convolution. The infimum is attained by [F2], and for every minimiser $y$ the conditional Euler relation $D u_{0} (y) = D L ((x - y) / t) = (x - y) / t$ is [F3]; both suppliers use only the bounded uniformly continuous data class.

3.1step 1.1algebra∎

The separate quadratic infimum. For $t > 0$ and all $x, y$ , completing the square gives $\frac{1}{2} ∣ y ∣^{2} + \frac{∣ x - y ∣^{2}}{2 t} = \frac{1 + t}{2 t} ∣ y - \frac{x}{1 + t} ∣^{2} + \frac{∣ x ∣^{2}}{2 (1 + t)}$ . Since the coefficient $(1 + t) / (2 t)$ is positive, the infimum over $y$ is attained uniquely at $y = x / (1 + t)$ with value $∣ x ∣^{2} / (2 (1 + t))$ . This is a direct computation for the unbounded datum $w_{0}$ and makes no assertion that $w_{0}$ lies in the domain of the Hopf--Lax operator.

Remarks

What is and is not applied. The bounded-data statements are applied only to bounded uniformly continuous $u_{0}$ ; the quadratic datum is treated by the displayed algebraic computation, which is the Moreau envelope of $\frac{1}{2} ∣ \cdot ∣^{2}$ and does not claim a Hopf--Lax solution for it.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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)