ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

Distance to the boundary solves the unit eikonal Dirichlet problem on the ball

Example

Let $n \geq 1$ and let $Ω = B (0, 1) \subseteq R^{n}$ be the open unit ball and let $d (x) : = 1 - ∣ x ∣ = dist (x, \partial Ω)$ . Then $d$ is Lipschitz with $∣ D d ∣ = 1$ at every $x \neq 0$ , continuous on $\overline{Ω}$ with $d = 0$ on $\partial Ω$ , and $d$ is a viscosity solution of the stationary eikonal equation with zero boundary data: $∣ D u ∣ = 1 in Ω, u = 0 on \partial Ω .$ At $x \neq 0$ the equation holds classically; at the centre the function has a peak, every $C^{1}$ test function $ϕ$ with $d - ϕ$ having a local maximum at $0$ satisfies $∣ D ϕ (0) ∣ \leq 1$ (the subsolution inequality), and no $C^{1}$ test function has $d - ϕ$ locally minimal at $0$ : a lower contact would require $⟨ D ϕ (0), h ⟩ \leq - ∣ h ∣$ for all $h$ , which is impossible, so no such contact exists and the supersolution test is vacuous at the centre. Hence $d$ is a viscosity solution. The example is the canonical nonsmooth boundary-value solution of the eikonal equation, obtained by cone comparisons at the centre rather than by an abstract existence theorem.

Verification

Given: $n \geq 1$ , the open unit ball $Ω = B (0, 1)$ , its boundary the unit sphere (Euclidean spheres and closed balls as subspaces of $R^{n}$ ), the distance function $d (x) = 1 - ∣ x ∣$ , the norm $∣ \cdot ∣$ (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms) and the inner product (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F1] The test-function definition of viscosity sub- and supersolutions of $∣ D u ∣ - 1 = 0$ , and its equivalent jet formulation (Viscosity subsolutions and supersolutions of a first-order equation and of the Cauchy problem, Viscosity testing by first-order jets, and closure of the jet inequality).

[F2] For $x \neq 0$ the map $x \mapsto ∣ x ∣$ is $C^{1}$ with gradient $x / ∣ x ∣$ of norm $1$ , as computed in The eikonal equation as a viscosity equation at a tip; hence $d$ is $C^{1}$ on $Ω ∖ {0}$ with $D d (x) = - x / ∣ x ∣$ and $∣ D d (x) ∣ = 1$ ; also $d$ is Lipschitz with constant $1$ by the triangle inequality (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

Proof technique: classical verification away from the centre and cone comparisons at the centre.

1.1F2

Classical region. For $x \neq 0$ the function $d$ is $C^{1}$ near $x$ with $∣ D d ∣ = 1$ by [F2], so it is a viscosity solution of $∣ D u ∣ = 1$ on the punctured ball by the classical-consistency argument of The eikonal equation as a viscosity equation at a tip.

1.2F1F2algebra

Upper contacts at the centre. Let $ϕ \in C^{1}$ with $d - ϕ$ having a local maximum at $0$ ; normalize $ϕ (0) = d (0) = 1$ . Then $1 - ∣ x ∣ \leq ϕ (x) = 1 + ⟨ D ϕ (0), x ⟩ + o (∣ x ∣)$ near $0$ , that is $⟨ D ϕ (0), x ⟩ \geq - ∣ x ∣ + o (∣ x ∣)$ ; substitute $x = a e$ and $x = - a e$ for a unit vector $e$ , divide by $a > 0$ , and let $a ↓ 0$ to obtain $∣ ⟨ D ϕ (0), e ⟩ ∣ \leq 1$ . Taking $e$ in the direction of $D ϕ (0)$ , when this gradient is nonzero, gives $∣ D ϕ (0) ∣ \leq 1$ . Hence every upper test satisfies the subsolution inequality $∣ D ϕ (0) ∣ - 1 \leq 0$ at the centre.

1.3F1F2algebra

No lower contact at the centre. If $d - ϕ$ had a local minimum at $0$ , the reversed inequality would give $⟨ D ϕ (0), x ⟩ \leq - ∣ x ∣ + o (∣ x ∣)$ for all $x$ near $0$ ; substituting $x = a e$ and $x = - a e$ , dividing by $a > 0$ and taking $a ↓ 0$ gives $⟨ D ϕ (0), e ⟩ \leq - 1$ and $⟨ D ϕ (0), e ⟩ \geq 1$ , an impossibility. Hence no lower $C^{1}$ test exists at the centre and the supersolution inequality holds vacuously.

2.1step 1.1step 1.2step 1.3F2∎

Boundary values and conclusion. For $x \in Ω$ and $y \in \partial Ω$ , the reverse triangle inequality gives $∣ x - y ∣ \geq 1 - ∣ x ∣$ . Equality is achieved at $y = x / ∣ x ∣$ when $x \neq 0$ , and at any unit vector when $x = 0$ , so $d (x) = dist (x, \partial Ω)$ . Since $∣ x ∣ \to 1$ along sequences approaching the unit sphere, the continuous extension of $d$ to $\overline{Ω}$ vanishes exactly on $\partial Ω$ . Steps 1.2 and 1.3 give the subsolution inequality everywhere and the supersolution inequality everywhere (vacuously at the centre, classically elsewhere by step 1.1), so $d$ is a viscosity solution of the unit eikonal equation with zero boundary data on the ball.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 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)
Alberto Bressan, Viscosity Solutions of Hamilton--Jacobi Equations and Optimal Control Problems, complete author lecture notes, Penn State University (PDF records Fall 2019 revision) (standard reference, not scraped)