Eq. (14), p. 783 — the expected cost of a fixed policy is the value of a linear program

Proved

RobustMDP.FiniteHorizon.expectedCost_lp

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-programmingmarkov-decision-processp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Fix an initial state $i_0$ , a controller policy $\pi=(\mathbf a_t)_{t\in T}$ and transition matrices $P=(P_t^a)_{a\in\mathcal A,\,t\in T}$ whose rows are probability vectors. Let $q=e_{i_0}$ ( $q(i_0)=1$ , $q(i)=0$ otherwise). Then the expected total cost $C_N(\pi,P)$ of (2) is the optimal value of the linear program

\max_{v_0,\dots,v_{N-1}}\ q^{\mathsf T}v_0\quad\text{s.t.}\quad v_t(i)\le c_t(i,\mathbf a_t(i))+\sum_j P_t^{\mathbf a_t(i)}(i,j)\,v_{t+1}(j),\quad i\in\mathcal X,\ t\in T, \tag{14}

with $v_N=c_N$ , and the maximum is attained.

The linear program links the probabilistic definition (2) of the cost to the backward recursions: letting the matrices vary over nature's admissible set turns (14) into problem (16).

Formalization Note The cost $C_N$ is the forward-distribution expectation of (2). The terminal condition $v_N=c_N$ is implicit on the page (the paper writes $\varphi_N(\pi,\tau)$ for $C_N(\pi,\tau)$ here). Since $q=e_{i_0}$ , the objective $q^{\mathsf T}v_0$ is written $v_0(i_0)$ . The maximum is stated with IsGreatest.

Preamble

import Mathlib
import Definitions.Def_RobustMDP_FiniteHorizon_Model
import Definitions.Def_RobustMDP_FiniteHorizon_expectedCost

Formal statement

namespace RobustMDP.FiniteHorizon

/-- The linear program (14), p. 783. For a given controller policy `π` and a given collection of
time-varying transition matrices `P = (P_t^a)` (every row a probability vector), the expected
total cost `C_N(π, P)` of (2) is the optimal value of
`max qᵀ v_0` over `v_0, …, v_{N-1}` subject to
`v_t(i) ≤ c_t(i, 𝐚_t(i)) + ∑_j P_t^{𝐚_t(i)}(i, j) v_{t+1}(j)` for all `i`, `t ∈ T`, with
`v_N = c_N` and `q = e_{i₀}` (so `qᵀ v_0 = v_0(i₀)`). -/
theorem expectedCost_lp {n N : ℕ} {A : Type} (M : Model n N A) (i₀ : Fin n)
    (π : ControlPolicy n N A) (P : Fin N → A → Fin n → Fin n → ℝ)
    (hP : ∀ t a i, P t a i ∈ stdSimplex ℝ (Fin n)) :
    IsGreatest
      {x : ℝ | ∃ v : Fin (N + 1) → Fin n → ℝ,
        v (Fin.last N) = M.terminalCost ∧
        (∀ t : Fin N, ∀ i, v t.castSucc i ≤
          M.cost t i (π t i) + ∑ j, P t (π t i) i j * v t.succ j) ∧
        x = v 0 i₀}
      (M.expectedCost i₀ π P) := by sorry

end RobustMDP.FiniteHorizon

Source

Nilim and El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Oper. Res. 53 (2005), p. 783, Eq. (14)

Read-back

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

Hypotheses. The statement fixes:

a model $M$ with $n$ states, $N$ stages and any action type $A$ , with stage costs $c_t$ and terminal cost $c_N$ ;
an initial state $i_0$ ;
a control policy $\pi$ ;
a real array $P_t^a(i,j)$ whose every row $P_t^a(i,\cdot)$ lies in the standard simplex.

$P$ is not required to take its rows from $M$ 's row sets $\mathcal{P}_i^a$ .

Conclusion. The expected cost $C_N(\pi,P)$ is the greatest element of the set of numbers $v_0(i_0)$ , taken over all sequences $v_0,\dots,v_N \in \mathbb{R}^n$ with $v_N = c_N$ and

v_t(i) \le c_t\big(i,\pi_t(i)\big) + \sum_j P_t^{\pi_t(i)}(i,j)\, v_{t+1}(j) \quad\text{for all } t<N \text{ and all states } i.

Here $C_N(\pi,P)$ is defined as

C_N(\pi,P) = \sum_{t<N}\sum_i \mu_t(i)\, c_t(i,\pi_t(i)) + \sum_i \mu_N(i)\, c_N(i),

where $\mu_0$ is the point mass at $i_0$ and

\mu_{t+1}(j) = \sum_i \mu_t(i)\, P_t^{\pi_t(i)}(i,j).

"Greatest element" means two things: $C_N(\pi,P)$ is attained by some feasible sequence, and it is at least every feasible $v_0(i_0)$ .

Degenerate cases.

$N = 0$ : the set is $\{c_N(i_0)\}$ and the cost is $c_N(i_0)$ .
$n = 0$ : no $i_0$ exists, so the statement has no instances.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph