Classical HJB verification

This example proves optimality for a one-dimensional deterministic control problem with quadratic control cost. The general verification theorem assumes a classical HJB solution and integrability along admissible paths.

Control problem

The model fixes a terminal time 1. Starting from (t₀,x₀), an admissible real-valued control a and state path x satisfy x'(s)=a(s). With running potential F and terminal cost g, total cost is

J(a)=\int_{t_0}^{1}\left(\frac{a(s)^2}{2}+F(s,x(s))\right)\,ds+g(x(1)).

The admissible-path structure records a continuous control, differentiable state, and integrability of the running cost.

Equation and verification

A classical solution satisfies

\partial_t u-\frac{(\partial_x u)^2}{2}+F=0, \qquad u(1,x)=g(x).

The verification theorem proves that a candidate satisfying this equation gives a lower bound on the cost of any admissible path. When a path follows the feedback a=-∂ₓu, its cost attains the bound and it is optimal. The general theorem states interval integrability of the value derivative along paths as an explicit hypothesis for the fundamental theorem of calculus.

Lean statement and hypotheses

HJB.lean

theorem verification_optimal {P : Problem} (U : ClassicalSolution P)
    {z : InitialCondition} (γ : AdmissiblePath P z)
    (hintγ : IntervalIntegrable (alongPathDerivative U γ) volume z.time 1)
    (hfeedback : ∀ s ∈ Icc z.time 1,
      γ.control s = -U.spaceDerivative s (γ.state s))
    (η : AdmissiblePath P z)
    (hintη : IntervalIntegrable (alongPathDerivative U η) volume z.time 1) :
    totalCost P z γ ≤ totalCost P z η

U contains the smoothness, derivative, equation, and terminal-condition proofs. The two paths start from the same initial condition z. The hypotheses hintγ and hintη require interval integrability of the value derivative along each path; hfeedback requires the first path to follow the minimizing control throughout the interval. Under these hypotheses its cost is no greater than the second path's cost.

Quadratic example

Take F=0 and g(x)=x²/2. The smooth candidate and its feedback are

u(t,x)=\frac{x^2}{2(2-t)}, \qquad a(t,x)=-\frac{x}{2-t}.

For an initial state (t₀,x₀), the example constructs the explicit trajectory with constant control a=-x₀/(2-t₀), proves the required integrability for every admissible path in this problem, and certifies that the feedback trajectory is optimal.

This is a deterministic control verification result. It does not yet include a population-dependent potential, a forward population equation, or a coupled MFG equilibrium theorem.