Corollary 1 — history dependent deterministic policies are adequate for the robust value function

Proved

RobustDP.FiniteHorizon.corollary1_deterministic

by mikedeng1 · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamic-programmingmarkov-decision-processesp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1robust-optimization

Let $\Pi_D$ be the set of history dependent deterministic policies of a finite horizon AMDP with horizon $N$ . For $n=0,\dots,N-1$ and every history $h_n$ ,

V^*_n(h_n)=\sup_{\pi\in\Pi_D}V^\pi_n(h_n),

where $V^*_n(h_n)$ is the supremum of $V^\pi_n(h_n)$ over all history dependent randomized policies.

Randomization therefore does not improve the robust value.

Preamble

import Mathlib
import Definitions.Def_RobustDP_FiniteHorizon_Value

Formal statement

namespace RobustDP.FiniteHorizon

/-- Corollary 1 (Iyengar, TR-2002-07, p. 7): the history dependent deterministic policies `Π_D`
are adequate: for `n = 0, …, N - 1`, `V*_n(h_n) = sup_{π ∈ Π_D} V^π_n(h_n)`, where `V*_n` is the
supremum over all history dependent randomized policies. -/
theorem corollary1_deterministic {S A : Type*} [Countable S] [Countable A] (M : AMDP S A) :
    ∀ n < M.N, ∀ h : History S A n,
      Vstar M n h = ⨆ π : {π : Policy M // IsDeterministic π}, V M π.1 n h := by sorry

end RobustDP.FiniteHorizon

Source

Iyengar, Robust dynamic programming, CORC Tech Report TR-2002-07 (rev. May 4, 2004), p. 7, Corollary 1

Human review

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

View graph