ExampleConstruction: AI-adaptedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Uniform Hamiltonian error for an evenly spaced compact-control grid

Statement

Let $A = [- 1, 1]$ , $b (a) = a$ , and $ℓ (a) = a^{2}$ . Then $H (p) = \max_{a \in [- 1, 1]} (- a p - a^{2}) = {\begin{cases} p^{2} / 4, & ∣ p ∣ \leq 2, \\ ∣ p ∣ - 1, & ∣ p ∣ > 2. \end{cases}$ For $m \geq 1$ , let $A_{m} = {- 1 + 2 r / m : r = 0, \dots, m}$ and let $H_{m} (p) = \max_{a \in A_{m}} (- a p - a^{2})$ . The uniform control-grid error satisfies $\sup_{p \in R} ∣ H_{m} (p) - H (p) ∣ \leq m^{- 2} .$ Thus $A_{m}$ satisfies the control approximation hypothesis of Periodic first-order controlled Hamilton–Jacobi Cauchy problem. For any continuous periodic initial datum, its semi-Lagrangian scheme falls under Convergence of the positive-interpolation and upwind first-order HJB schemes whenever the stated mesh restrictions also hold.

Facts & Assumptions

Given: The compact control set and coefficient functions in the statement and the Hamiltonian convention of Periodic first-order controlled Hamilton–Jacobi Cauchy problem.

[F1]

For $g_{p} (a) = - a p - a^{2}$ , completing the square gives $g_{p} (a) = p^{2} / 4 - (a + p / 2)^{2}$ ; hence its maximizer is the projection of $- p / 2$ onto $[- 1, 1]$ (Periodic first-order controlled Hamilton–Jacobi Cauchy problem).

[F2]

If $∣ p ∣ \leq 2$ , a nearest point of the evenly spaced grid $A_{m}$ is at distance at most $1 / m$ from $- p / 2$ ; if $∣ p ∣ > 2$ , the maximizing endpoint is included in $A_{m}$ (finite-grid definition in the statement).

[F3]

The convergence theorem requires the Hamiltonian errors to vanish on bounded momentum sets and the semi-Lagrangian mesh condition $h_{\max}^{} / τ \to 0$ (Positive-interpolation semi-Lagrangian update for first-order HJB equations, Convergence of the positive-interpolation and upwind first-order HJB schemes).

Proof

1.1F1givenalgebra

Completing the square as in [F1], the unconstrained maximizing control is $a_{*} = - p / 2$ . It lies in $[- 1, 1]$ exactly when $∣ p ∣ \leq 2$ , where substitution gives $H (p) = p^{2} / 4$ . If $p > 2$ , the concave quadratic is maximized at $a = - 1$ and gives $p - 1$ ; if $p < - 2$ , it is maximized at $a = 1$ and gives $- p - 1$ . This proves the displayed formula.

2.1F1F2F3step 1.1algebra∎

For $∣ p ∣ \leq 2$ , choose a nearest $a_{m} \in A_{m}$ to $a_{*}$ . Then $H (p) - H_{m} (p) = (a_{m} - a_{*})^{2} \leq m^{- 2}$ by [F1] and [F2]. For $∣ p ∣ > 2$ , the maximizing endpoint belongs to $A_{m}$ , so $H_{m} (p) = H (p)$ . Also $H_{m} (p) \leq H (p)$ since $A_{m} \subset A$ . Taking the supremum proves the global error bound. Because $m^{- 2} \to 0$ , condition [F3] is satisfied for every bounded momentum set (in fact for all momenta), so the stated convergence theorem applies along any mesh family satisfying its remaining hypotheses.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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

Kristian Debrabant and Espen R. Jakobsen, Semi-Lagrangian schemes for linear and fully non-linear Hamilton-Jacobi-Bellman equations (standard reference, not scraped)
Hung Vinh Tran, Hamilton–Jacobi Equations: Theory and Applications, 2020 author manuscript (standard reference, not scraped)