Discrete adjoint first-variation inequality

Proved

BertsekasDP.discrete_adjoint_variational_inequality

by Yuning · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

adjointdiscreteminimumprinciplevariationalinequality

Consider a smooth finite-horizon discrete-time optimal-control problem with convex stagewise control sets. Fix an optimal feasible state-control trajectory and a supplied adjoint sequence satisfying the terminal transversality condition and the backward costate recursion. Then, at every stage $k<N$ and for every feasible control $u\in U_k$ , the Hamiltonian control gradient satisfies

\left\langle \nabla_u H_k(x_k^*,u_k^*,p_{k+1}),\;u-u_k^*\right\rangle \ge 0.

This lemma isolates the finite-dimensional first-variation argument: perturb one control along a segment in the convex set, propagate the resulting state variation through the remaining dynamics, and cancel the propagated terms using the adjoint recursion. It can be reused independently of how the adjoint sequence is constructed.

Formalization Note Optimality is quantified over all feasible infinite sequences, while the cost and the conclusion depend only on stages below $N$ .

Preamble

import Mathlib

open scoped RealInnerProductSpace

Formal statement

namespace BertsekasDP

/-- The finite-horizon first-variation step for a supplied discrete adjoint sequence. -/
theorem discrete_adjoint_variational_inequality {n m N : ℕ}
    (f : ℕ → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m) →
      EuclideanSpace ℝ (Fin n))
    (g : ℕ → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m) → ℝ)
    (gN : EuclideanSpace ℝ (Fin n) → ℝ)
    (U : ℕ → Set (EuclideanSpace ℝ (Fin m)))
    (hUconv : ∀ k, Convex ℝ (U k))
    (hf : ∀ k, ContDiff ℝ 1 (Function.uncurry (f k)))
    (hg : ∀ k, ContDiff ℝ 1 (Function.uncurry (g k)))
    (hgN : ContDiff ℝ 1 gN)
    (x0 : EuclideanSpace ℝ (Fin n))
    (ustar : ℕ → EuclideanSpace ℝ (Fin m))
    (xstar : ℕ → EuclideanSpace ℝ (Fin n))
    (hx0 : xstar 0 = x0)
    (hdyn : ∀ k < N, xstar (k + 1) = f k (xstar k) (ustar k))
    (humem : ∀ k < N, ustar k ∈ U k)
    (hopt : ∀ (u : ℕ → EuclideanSpace ℝ (Fin m))
      (x : ℕ → EuclideanSpace ℝ (Fin n)),
      x 0 = x0 → (∀ k < N, x (k + 1) = f k (x k) (u k)) →
      (∀ k < N, u k ∈ U k) →
      gN (xstar N) + ∑ k ∈ Finset.range N, g k (xstar k) (ustar k) ≤
        gN (x N) + ∑ k ∈ Finset.range N, g k (x k) (u k))
    (p : ℕ → EuclideanSpace ℝ (Fin n))
    (hpN : p N = gradient gN (xstar N))
    (hpadj : ∀ k < N, p k =
      gradient (fun y => g k y (ustar k) + ⟪p (k + 1), f k y (ustar k)⟫)
        (xstar k)) :
    ∀ k < N, ∀ u ∈ U k,
      0 ≤ ⟪gradient
            (fun v => g k (xstar k) v + ⟪p (k + 1), f k (xstar k) v⟫)
            (ustar k),
          u - ustar k⟫ := by
  sorry

end BertsekasDP

Source

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Proposition 3.3.2 and its first-variation derivation.

View graph