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

Failure of the supersolution test for the lower envelope allows a local bump

Statement

Let $U \subseteq R^{n + 1}$ be open, let $H : U \times R^{n} \to R$ be continuous, and let $w : U \to R$ be an upper semicontinuous viscosity subsolution of $u_{t} + H (x, t, D u) = 0$ in $U$ . Suppose the lower semicontinuous envelope $w_{*}$ fails the supersolution test at $\hat{z} \in U$ in the following precise sense: $w_{*} (\hat{z}) \in R$ and there is $ϕ \in C^{1} (U)$ such that $w_{*} - ϕ$ has a local minimum at $\hat{z}$ and $ϕ_{t} (\hat{z}) + H (\hat{z}, D ϕ (\hat{z})) < 0.$ Then for every sufficiently small $κ > 0$ there is a viscosity subsolution $W_{κ}$ of the same equation in $U$ with $W_{κ} \geq w on U, \sup_{U} (W_{κ} - w) > 0, W_{κ} = w on {z \in U : ∣ z - \hat{z} ∣ \geq κ} .$ Moreover $W_{κ}$ can be taken to be $\max (w, χ)$ on a small ball around $\hat{z}$ and $w$ outside it, where $χ$ is a classical subsolution with $χ (\hat{z}) = w_{*} (\hat{z}) + δ$ for some $δ > 0$ . No choice principle is used.

Facts & Assumptions

Given: Open $U \subseteq R^{n + 1}$ , continuous $H : U \times R^{n} \to R$ , an upper semicontinuous viscosity subsolution $w : U \to R$ , its lower envelope $w_{*}$ , a point $\hat{z} \in U$ with $w_{*} (\hat{z}) \in R$ and a $C^{1}$ test $ϕ$ with $w_{*} - ϕ$ having a local minimum at $\hat{z}$ and $c : = - (ϕ_{t} (\hat{z}) + H (\hat{z}, D ϕ (\hat{z}))) > 0$ .

[F1]

$w_{*} (z) = \sup_{r > 0} \inf {w (y) : ∣ y - z ∣ \leq r}$ is the lower semicontinuous envelope of $w$ , it satisfies $w_{*} \leq w$ pointwise, and for every $η > 0$ there are points $z$ arbitrarily close to $\hat{z}$ with $w (z) < w_{*} (\hat{z}) + η$ (Upper and lower semicontinuous envelopes by local limsup and liminf).

[F2]

A finite maximum of finitely many viscosity subsolutions of the equation in an open set is a viscosity subsolution (Finite maxima of subsolutions and finite minima of supersolutions); a $C^{1}$ function with $χ_{t} + H (z, D χ) \leq 0$ pointwise is a viscosity subsolution of the same equation (Classical solutions are viscosity solutions and differentiable viscosity solutions solve the equation pointwise, Viscosity subsolutions and supersolutions of a first-order equation and of the Cauchy problem).

[F3]

A continuous function $f$ with $f (\hat{z}) < 0$ is negative on a neighbourhood of $\hat{z}$ ; here the function in question is $z \mapsto ϕ_{t} (z) + H (z, D ϕ (z))$ (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, Viscosity subsolutions and supersolutions of a first-order equation and of the Cauchy problem for the smoothness conventions).

Proof

technique · a strict test-function bump plus the finite-maximum rule

1.1F1F2F3algebra

The bump function. Fix $κ > 0$ with $\overline{B} (\hat{z}, κ) \subseteq U$ and choose $r \in (0, κ]$ small. For $γ > 0$ put $\tilde{ϕ} (z) : = ϕ (z) - γ ∣ z - \hat{z} ∣^{4}$ , so that $\tilde{ϕ} \in C^{1} (U)$ , $\tilde{ϕ} (\hat{z}) = ϕ (\hat{z})$ and $D \tilde{ϕ} (\hat{z}) = D ϕ (\hat{z})$ ; shrinking $r$ if necessary and using [F3], we may assume ${\tilde{ϕ}}_{t} (z) + H (z, D \tilde{ϕ} (z)) \leq - c / 2 < 0$ for all $z \in \overline{B} (\hat{z}, r)$ , so every vertical translate of $\tilde{ϕ}$ is a classical, hence viscosity, subsolution there. Since $w_{*} - ϕ$ has a local minimum at $\hat{z}$ , after shrinking $r$ we have $w_{*} (z) - \tilde{ϕ} (z) \geq m + γ ∣ z - \hat{z} ∣^{4}$ for $z \in \overline{B} (\hat{z}, r)$ , where $m : = w_{*} (\hat{z}) - ϕ (\hat{z})$ . Choose $0 < δ < γ (r / 2)^{4}$ and define $χ : = \tilde{ϕ} + m + δ$ , a classical subsolution on $\overline{B} (\hat{z}, r)$ with $χ (\hat{z}) = w_{*} (\hat{z}) + δ$ . On the annulus $r / 2 \leq ∣ z - \hat{z} ∣ \leq r$ we have $w_{*} (z) \geq \tilde{ϕ} (z) + m + γ ∣ z - \hat{z} ∣^{4} \geq χ (z) - δ + γ (r / 2)^{4} > χ (z)$ , and since $w_{*} \leq w$ by [F1] this gives $χ < w$ there. By continuity of $χ$ , choose $r_{0} \in (0, r / 2)$ so that $χ (z) > w_{*} (\hat{z}) + δ / 2$ whenever $∣ z - \hat{z} ∣ < r_{0}$ . The lower-envelope definition [F1] gives a point $z_{0}$ in this ball with $w (z_{0}) < w_{*} (\hat{z}) + δ / 2 < χ (z_{0})$ .

2.1step 1.1F2algebra∎

The bump is a subsolution. Define $W : = \max (w, χ)$ on $B (\hat{z}, r)$ and $W : = w$ on $U ∖ B (\hat{z}, r)$ ; this is well defined because on the sphere $∣ z - \hat{z} ∣ = r$ one has $χ < w$ by step 1.1. Then $W \geq w$ on $U$ , and $\sup_{U} (W - w) > 0$ at the point $z_{0}$ of step 1.1. On the ball $B (\hat{z}, r)$ the function $W$ is the maximum of the viscosity subsolution $w$ and the classical, hence viscosity, subsolution $χ$ , so it is a viscosity subsolution there by [F2]; on the exterior of $\overline{B} (\hat{z}, r)$ it equals the subsolution $w$ ; and near every point of the sphere it equals $w$ , which is a subsolution, so by locality of the definition $W$ is a viscosity subsolution on all of $U$ . Since $χ < w$ on the annulus, $W = w$ outside $B (\hat{z}, r) \subseteq B (\hat{z}, κ)$ , that is $W = w$ on ${z : ∣ z - \hat{z} ∣ \geq κ}$ ; and $W$ is upper semicontinuous as a maximum of the upper semicontinuous $w$ and the continuous $χ$ .

Depends on

Used by

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

Dependency tree · two levels

38 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

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