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.

Time-space barriers enforce the initial trace for the Cauchy problem

Statement

Let $n \geq 1$ , $T > 0$ , $O \subseteq R^{n}$ open, $Z = O \times (0, T)$ , let $H : O \times [0, T] \times R^{n} \to R$ be continuous, and let $u_{0} \in C^{1} (O)$ have bounded gradient. Assume $C_{0} : = \sup_{x \in O, 0 \leq t \leq T} ∣ H (x, t, D u_{0} (x)) ∣ < \infty$ . Define $ϕ_{\pm} (x, t) : = u_{0} (x) \pm C_{0} t$ . Then: (1) $ϕ_{-}$ is a classical subsolution and $ϕ_{+}$ a classical supersolution in $Z$ , each with initial datum $u_{0}$ ; (2) if $w : Z \to R$ is locally bounded with $ϕ_{-} \leq w \leq ϕ_{+}$ on $Z$ , then for every $x \in O$ the relaxed limits satisfy ${lim inf}_{\begin{array}{c} (y, s) \to (x, 0) \\ s > 0 \end{array}} w (y, s) \geq u_{0} (x) \geq {lim sup}_{\begin{array}{c} (y, s) \to (x, 0) \\ s > 0 \end{array}} w (y, s),$ so both equal $u_{0} (x)$ ; (3) consequently $w$ satisfies the relaxed initial condition for the Cauchy problem in both directions, and any continuous extension of $w$ to the initial face takes the value $u_{0}$ pointwise. No choice principle is used.

Facts & Assumptions

Given: Open $O \subseteq R^{n}$ , $T > 0$ , continuous $H : O \times [0, T] \times R^{n} \to R$ , $u_{0} \in C^{1} (O)$ with bounded gradient, $C_{0} = \sup_{O \times [0, T]} ∣ H (x, t, D u_{0} (x)) ∣ < \infty$ , the barriers $ϕ_{\pm} = u_{0} \pm C_{0} t$ , and a locally bounded $w : Z \to R$ with $ϕ_{-} \leq w \leq ϕ_{+}$ .

[F1]

If a $C^{1}$ function satisfies the differential inequality pointwise on the open set $Z$ , then it satisfies the corresponding viscosity test inequality: at a local contact with another $C^{1}$ function, Fermat's theorem makes their first derivatives equal (Viscosity subsolutions and supersolutions of a first-order equation and of the Cauchy problem, Fermat's theorem: an interior differentiable local extremum has zero gradient).

[F2]

The functions $(x, t) \mapsto u_{0} (x) \pm C_{0} t$ are $C^{1}$ on $Z$ , with time derivatives $\pm C_{0}$ and spatial gradient $D u_{0} (x)$ ; since $u_{0}$ is continuous on $O$ , they extend continuously to the initial face $O \times {0}$ with value $u_{0}$ ( $C^{k}$ maps and multi-index derivative notation in Euclidean space).

[F3]

The relaxed initial conditions for a subsolution and a supersolution of the Cauchy problem are stated as limsup and liminf over $(y, s) \to (x, 0)$ with $s > 0$ (Viscosity subsolutions and supersolutions of a first-order equation and of the Cauchy problem).

Proof

technique · explicit affine-in-time barriers and continuity of the datum

1.1F1F2algebra

The barriers are pointwise classical sub- and supersolutions on $Z$ . By [F2], $ϕ_{\pm}$ are $C^{1}$ there, with $(ϕ_{\pm})_{t} = \pm C_{0}$ and $D ϕ_{\pm} = D u_{0}$ . The definition of $C_{0}$ gives $- C_{0} \leq H (x, t, D u_{0} (x)) \leq C_{0}$ for every $(x, t) \in O \times [0, T]$ , so $(ϕ_{-})_{t} + H (x, t, D ϕ_{-}) = - C_{0} + H (x, t, D u_{0} (x)) \leq 0$ and $(ϕ_{+})_{t} + H (x, t, D ϕ_{+}) = C_{0} + H (x, t, D u_{0} (x)) \geq 0$ pointwise on $Z$ . By [F1] these pointwise inequalities imply the viscosity test inequalities, and [F2] gives the pointwise initial values. No continuity on the lateral boundary $\partial O \times [0, T]$ is needed.

2.1step 1.1algebra

The squeeze at the initial face. Fix $x \in O$ . For $(y, s) \in Z$ the pointwise bounds give $ϕ_{-} (y, s) = u_{0} (y) - C_{0} s \leq w (y, s) \leq u_{0} (y) + C_{0} s = ϕ_{+} (y, s)$ . As $(y, s) \to (x, 0)$ with $s > 0$ we have $s \to 0$ and $y \to x$ , so by continuity of $u_{0}$ at $x$ both $u_{0} (y) - C_{0} s \to u_{0} (x)$ and $u_{0} (y) + C_{0} s \to u_{0} (x)$ ; the squeeze therefore gives $lim inf w \geq u_{0} (x)$ and $lim sup w \leq u_{0} (x)$ , both relaxed limits being taken along $s > 0$ .

3.1step 2.1F3∎

Conclusion. By step 2.1 the two relaxed limits both equal $u_{0} (x)$ , which is exactly the bisided relaxed initial condition of [F3]; in particular a continuous extension of $w$ to $O \times {0}$ must take the value $u_{0}$ there. This is the two-barrier boundary control used by the Perron construction.

Remarks

Sharpness of the hypothesis. The boundedness of $C_{0}$ is what makes the barriers classical; it holds, for example, when $H$ is uniformly bounded on $O \times [0, T] \times {∣ p ∣ \leq ∥ D u_{0} ∥_{\infty}}$ . Boundedness of $O$ or boundedness for each fixed momentum alone does not supply that uniform bound. The barriers are the model two-sided control of the initial face and are used in the Perron existence theorem.

Depends on

Used by

Perron's method for the Cauchy problem: existence between two barriers Theorem

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

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)
Michael G. Crandall, Hitoshi Ishii and Pierre-Louis Lions, User's guide to viscosity solutions of second order partial differential equations, Bulletin of the American Mathematical Society 27 (1992), 1--67 (complete article) (standard reference, not scraped)