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 Hopf--Lax operators form a semigroup (dynamic programming)

Statement

Let $H : R^{n} \to R$ be convex and superlinear with Legendre transform $L$ , and let $u_{0} : R^{n} \to R$ be bounded and uniformly continuous. Then for all $t, s \geq 0$ the Hopf--Lax operators of The Hopf--Lax operator and the Hopf--Lax formula satisfy $Q_{t + s} u_{0} = Q_{t} (Q_{s} u_{0}) = Q_{s} (Q_{t} u_{0}) pointwise on R^{n},$ where the inner operators are applied to the bounded uniformly continuous function $Q_{s} u_{0}$ (or $Q_{t} u_{0}$ ) produced by The Hopf--Lax operator preserves a modulus of continuity. Equivalently, for all $t, s > 0$ and $x \in R^{n}$ the short-time variational principle holds: $Q_{t + s} u_{0} (x) = \inf_{z \in R^{n}} {Q_{s} u_{0} (z) + t L (\frac{x - z}{t})} .$ The family $(Q_{t})_{t \geq 0}$ is therefore a semigroup with $Q_{0} = i d$ on the bounded uniformly continuous data. No choice principle is used.

Facts & Assumptions

Given: A convex superlinear $H$ with Legendre transform $L$ , a bounded uniformly continuous $u_{0}$ , the operators $Q_{t}$ of The Hopf--Lax operator and the Hopf--Lax formula, and $t, s > 0$ .

[F1]

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

[F2]

$L$ is convex: $L ((1 - λ) w_{1} + λ w_{2}) \leq (1 - λ) L (w_{1}) + λ L (w_{2})$ for all $w_{1}, w_{2}$ and $λ \in [0, 1]$ (Convex and strictly convex functions on Euclidean convex sets).

[F3]

$Q_{s} u_{0}$ is bounded and has the modulus of continuity of $u_{0}$ ; in particular it is bounded and uniformly continuous, so the inner operator $Q_{t}$ is defined on it (The Hopf--Lax operator preserves a modulus of continuity).

Proof

technique · the two-point convexity inequality with weights adapted to $t$ and $s$

1.1F1F2F3algebra

The inequality $Q_{t + s} u_{0} \leq Q_{t} (Q_{s} u_{0})$ . Fix $y, z \in R^{n}$ and write $(x - y) / (t + s) = \frac{t}{t + s} \frac{x - z}{t} + \frac{s}{t + s} \frac{z - y}{s}$ , a convex combination with weights $t / (t + s)$ and $s / (t + s)$ ; by [F2], $L ((x - y) / (t + s)) \leq \frac{t}{t + s} L ((x - z) / t) + \frac{s}{t + s} L ((z - y) / s)$ . Multiplying by $t + s$ and adding $u_{0} (y)$ gives $u_{0} (y) + (t + s) L ((x - y) / (t + s)) \leq [u_{0} (y) + s L ((z - y) / s)] + t L ((x - z) / t)$ . Taking the infimum over $y$ on the left and over $y$ and then $z$ on the right (the double infimum is an infimum over pairs, legitimate for real infima by [F1]) yields $Q_{t + s} u_{0} (x) \leq \inf_{z} {Q_{s} u_{0} (z) + t L ((x - z) / t)} = Q_{t} (Q_{s} u_{0}) (x)$ .

1.2F1F2F3algebra

The reverse inequality. Fix $y \in R^{n}$ and choose the segment point $z : = y + \frac{s}{t + s} (x - y)$ , for which $\frac{z - y}{s} = \frac{x - z}{t} = \frac{x - y}{t + s}$ . Then $u_{0} (y) + s L ((z - y) / s) + t L ((x - z) / t) = u_{0} (y) + (t + s) L ((x - y) / (t + s))$ ; taking the infimum over $y$ gives $Q_{t} (Q_{s} u_{0}) (x) \leq Q_{t + s} u_{0} (x)$ .

2.1step 1.1step 1.2F1F3∎

Conclusion. Steps 1.1 and 1.2 give $Q_{t + s} u_{0} = Q_{t} (Q_{s} u_{0})$ for all $t, s > 0$ . The operator $Q_{s}$ maps the bounded uniformly continuous datum to a bounded uniformly continuous function by [F3], so the composition is well defined; swapping the roles of $t$ and $s$ in the same computation gives $Q_{t + s} u_{0} = Q_{s} (Q_{t} u_{0})$ , and the case $t = 0$ or $s = 0$ is the definition $Q_{0} = i d$ of [F1]. Hence $(Q_{t})_{t \geq 0}$ is a semigroup of operators on the bounded uniformly continuous data, and the displayed short-time variational principle is the identity $Q_{t} (Q_{s} u_{0}) = Q_{t + s} u_{0}$ written out.

Remarks

Choice. The two inequalities are computed by taking infima over explicit sets of reals; the segment point $z$ is given by a formula, so nothing is selected and no choice principle is used.
Why the datum class is preserved. The semigroup statement needs the inner operator to be applied to a bounded uniformly continuous function, which is exactly the content of The Hopf--Lax operator preserves a modulus of continuity together with the boundedness following from $u_{0}$ bounded and $L \geq - H (0)$ .

Depends on

Used by

Dependency tree · two levels

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