Discrete-time Minimum Principle (Prop. 3.3.2)

Proved

BertsekasDP.discrete_minimum_principle

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

discreteminimumprinciplevariationalinequality

Proposition 3.3.2 (Discrete-Time Minimum Principle). Consider the deterministic discrete-time problem of minimizing

g_N(x_N) + \sum_{k=0}^{N-1} g_k(x_k, u_k) \qquad \text{subject to} \qquad x_{k+1} = f_k(x_k,u_k), \quad x_0 \text{ given}, \quad u_k \in U_k,

with all $f_k$ , $g_k$ and $g_N$ continuously differentiable and every constraint set $U_k$ convex. Suppose $(u_0^*, \dots, u_{N-1}^*)$ is optimal, with corresponding trajectory $(x_0^*, \dots, x_N^*)$ . Define the stage Hamiltonians $H_k(x,u,p) = g_k(x,u) + \langle p, f_k(x,u)\rangle$ and the adjoint sequence backward by

p_N \;=\; \nabla g_N(x_N^*), \qquad p_k \;=\; \nabla_x H_k\bigl(x_k^*, u_k^*, p_{k+1}\bigr).

Then for every stage $k < N$ the variational inequality holds:

\bigl\langle \nabla_u H_k\bigl(x_k^*, u_k^*, p_{k+1}\bigr), \; u - u_k^* \bigr\rangle \;\ge\; 0 \qquad \text{for all } u \in U_k .

This is the discrete-time shadow of the Minimum Principle, and the natural warm-up target of this mission: it needs only finite-dimensional calculus, with no ODE theory, yet exhibits the same adjoint structure. Convexity of $U_k$ is what turns the first-order condition into a variational inequality over the whole constraint set; when $U_k = \mathbb{R}^m$ it reduces to stationarity, $\nabla_u H_k = 0$ .

Formalization Note The conclusion is a variational inequality, strictly weaker than the statement that $u_k^*$ minimizes $H_k$ over $U_k$ — the source derives the minimization form only under the additional convexity of $H_k$ in $u$ . Optimality is assumed against all feasible sequences with the same initial state. Gradients are Mathlib's, classical here since the data are $C^1$ ; with $N = 0$ every claim is vacuous.

Preamble

import Mathlib

Formal statement

namespace BertsekasDP

open scoped RealInnerProductSpace

theorem discrete_minimum_principle {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),
      p N = gradient gN (xstar N) ∧
      (∀ 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

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Setting. Fix natural numbers $n, m, N \ge 0$ (all implicit; $N = 0$ is allowed). Given are:

time-indexed dynamics $f_k : \mathbb{R}^n \times \mathbb{R}^m \to \mathbb{R}^n$ and stage costs $g_k : \mathbb{R}^n \times \mathbb{R}^m \to \mathbb{R}$ , defined for every $k \in \mathbb{N}$ (not only $k < N$ ), each assumed jointly $C^1$ as a function of the pair $(x, u)$ on the product space, for every $k \in \mathbb{N}$ ;
a terminal cost $g_N^{\mathrm{term}} : \mathbb{R}^n \to \mathbb{R}$ (a separate function, written gN; despite the name it is not $g$ at index $N$ ), assumed $C^1$ ;
control-constraint sets $U_k \subseteq \mathbb{R}^m$ for every $k \in \mathbb{N}$ , each assumed convex (convexity only; a $U_k$ may be empty, though then the membership hypotheses below become unsatisfiable for $k < N$ when $N > 0$ );
an initial state $x_0 \in \mathbb{R}^n$ , and candidate sequences $u^* : \mathbb{N} \to \mathbb{R}^m$ , $x^* : \mathbb{N} \to \mathbb{R}^n$ (defined for all indices, but constrained only as stated below).

Hypotheses on the candidate. $x^*_0 = x_0$ ; for every $k < N$ , $x^*_{k+1} = f_k(x^*_k, u^*_k)$ ; for every $k < N$ , $u^*_k \in U_k$ . (Values $u^*_k$ for $k \ge N$ and $x^*_k$ for $k > N$ are unconstrained, except that $x^*_N$ is determined by the dynamics when $N > 0$ .)

Optimality hypothesis. For every pair of sequences $u : \mathbb{N} \to \mathbb{R}^m$ , $x : \mathbb{N} \to \mathbb{R}^n$ satisfying $x_0^{} = x_0$ (same initial state), $x_{k+1} = f_k(x_k, u_k)$ for all $k < N$ , and $u_k \in U_k$ for all $k < N$ , one has

g_N^{\mathrm{term}}(x^*_N) + \sum_{k=0}^{N-1} g_k(x^*_k, u^*_k) \;\le\; g_N^{\mathrm{term}}(x_N) + \sum_{k=0}^{N-1} g_k(x_k, u_k).

This is a global comparison against all such sequences (a non-strict inequality); no local-optimality weakening is involved.

Conclusion. There exists a sequence $p : \mathbb{N} \to \mathbb{R}^n$ (an adjoint/costate sequence; its values at indices other than those mentioned are entirely unconstrained) such that:

$p_N = \nabla g_N^{\mathrm{term}}(x^*_N)$ ;
for every $k < N$ :

p_k = \nabla_y\Big[\, g_k(y, u^*_k) + \langle p_{k+1},\, f_k(y, u^*_k)\rangle \,\Big]\Big|_{y = x^*_k},

i.e. $p_k$ equals the gradient, at $x^*_k$ , of the map $y \mapsto g_k(y, u^*_k) + \langle p_{k+1}, f_k(y, u^*_k)\rangle$ (control frozen at $u^*_k$ , next costate frozen at $p_{k+1}$ ); 3. for every $k < N$ and every $u \in U_k$ :

0 \;\le\; \Big\langle \nabla_v\Big[\, g_k(x^*_k, v) + \langle p_{k+1},\, f_k(x^*_k, v)\rangle \,\Big]\Big|_{v = u^*_k},\;\; u - u^*_k \Big\rangle,

i.e. the gradient in the control variable of the same Hamiltonian-like expression, evaluated at $u^*_k$ with state frozen at $x^*_k$ , has nonnegative inner product with every feasible direction $u - u^*_k$ , $u \in U_k$ (a variational-inequality / first-order stationarity condition, not a minimization claim).

Edge cases: when $N = 0$ , all " $\forall k < N$ " hypotheses and conclusions are vacuous, the optimality hypothesis is trivially true, and the conclusion reduces to the existence of some $p$ with $p_0 = \nabla g_N^{\mathrm{term}}(x^*_0)$ , which is always satisfiable. The gradients above are Mathlib total gradients (junk value $0$ at non-differentiable points), though under the stated $C^1$ hypotheses the relevant maps are differentiable. The theorem's proof is sorry (it is stated, not proved).

Human review

Endorsed by Community (Bot) · Sep 7, 2026
Endorsed by Shuze Chen · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph