§6.1, p. 791 — for $\beta\ge\max_i(-\log q_i)$ the entropy set is the whole simplex and the worst case is $v_{\max}$

Proved

RobustMDP.EntropyInner.whole_simplex

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

kullback-leibler-divergencep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1robust-optimization

Let $q\in\Delta_n$ with $q(j)>0$ for all $j$ , let $\beta>0$ and $v\in\mathbb R^n$ . Let $\mathcal P=\{p\in\Delta_n : D(p\|q)\le\beta\}$ .

The quantity $\max_i(-\log q_i)$ is the maximum of the relative entropy over the simplex:

\max_{p\in\Delta_n} D(p\|q) = \max_i(-\log q_i),

and the maximum is attained. 2. If $\beta\ge\max_i(-\log q_i)$ , then $\mathcal P=\Delta_n$ and the worst-case value of $p^{\mathsf T}v$ over $\mathcal P$ is

\max_{p\in\mathcal P} p^{\mathsf T}v = v_{\max} := \max_j v(j),

again attained.

This identifies the regime in which the entropy constraint is inactive and the robust inner problem ignores the nominal distribution $q$ .

Formalization Note Both maxima are stated with IsGreatest (the value lies in the image and bounds it from above); $\max_i(-\log q_i)$ is the indexed supremum ⨆ i, -Real.log (q i) over the finite index set.

Preamble

import Mathlib
import Definitions.Def_RobustMDP_EntropyInner_klBall
import Definitions.Def_RobustMDP_EntropyInner_dualFunction

Formal statement

namespace RobustMDP.EntropyInner

/-- §6.1 (Nilim–El Ghaoui 2005, p. 791). Let `q ∈ Δₙ` with `q > 0` and `β > 0`.
(a) `maxᵢ (−log qᵢ)` is the maximum of `p ↦ D(p‖q)` over the simplex `Δₙ` (attained).
(b) If `β ≥ maxᵢ (−log qᵢ)`, the entropy set `𝒫 = {p ∈ Δₙ : D(p‖q) ≤ β}` is the whole simplex, and
the worst-case value of `pᵀv` over `𝒫` is `v_max = maxⱼ v(j)` (attained). -/
theorem whole_simplex {n : ℕ} (q v : Fin n → ℝ) (β : ℝ)
    (hq : q ∈ stdSimplex ℝ (Fin n)) (hq_pos : ∀ j, 0 < q j) (hβ : 0 < β) :
    IsGreatest ((fun p => klDiv p q) '' stdSimplex ℝ (Fin n)) (⨆ i, -Real.log (q i)) ∧
    ((⨆ i, -Real.log (q i)) ≤ β →
      klBall q β = stdSimplex ℝ (Fin n) ∧
      IsGreatest ((fun p : Fin n → ℝ => ∑ j, p j * v j) '' klBall q β) (vmax v)) := by sorry

end RobustMDP.EntropyInner

Source

Nilim and El Ghaoui, Robust Control of Markov Decision Processes with Uncertain Transition Matrices, Oper. Res. 53 (2005), p. 791, §6.1, last paragraph

Read-back

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

Setting. Let $n \in \mathbb{N}$ , let $q, v \in \mathbb{R}^n$ and let $\beta \in \mathbb{R}$ . Assume:

$q \in \Delta_n$ , where $\Delta_n = \{p : p_j \ge 0,\ \sum_j p_j = 1\}$ is the probability simplex;
$q_j > 0$ for every $j$ ;
$\beta > 0$ .

Notation.

The divergence is $D(p\,\|\,q) = \sum_j p_j \log(p_j/q_j)$ , with the convention that a term with $p_j = 0$ contributes $0$ . Since $q_j > 0$ , no other convention is involved for $p \in \Delta_n$ .
The set $\mathcal{B}(q,\beta) = \{p \in \Delta_n : D(p\,\|\,q) \le \beta\}$ .
$v_{\max} = \max_j v_j$ , the supremum of the coordinates of $v$ .
$M = \sup_i(-\log q_i)$ . Since every $q_i > 0$ , this is the largest of the real numbers $-\log q_i$ .

Conclusion (a). $M$ is the greatest element of the set of values $\{D(p\,\|\,q) : p \in \Delta_n\}$ . That is:

$D(p\,\|\,q) \le M$ for every $p \in \Delta_n$ ;
some $p \in \Delta_n$ has $D(p\,\|\,q) = M$ .

Conclusion (b). If $M \le \beta$ , then both of the following hold:

$\mathcal{B}(q,\beta) = \Delta_n$ , as sets;
$v_{\max}$ is the greatest element of $\{\sum_j p_j v_j : p \in \mathcal{B}(q,\beta)\}$ , meaning:

\sum_j p_j v_j \le v_{\max}\ \text{ for all } p \in \mathcal{B}(q,\beta), \qquad \text{and } \ \sum_j p_j v_j = v_{\max} \ \text{ for some } p \in \mathcal{B}(q,\beta).

The vector $v$ is arbitrary. The hypothesis $\beta > 0$ is assumed throughout, including in part (a), where $\beta$ does not appear.

Degenerate cases.

$n = 0$ : impossible, since $q \in \Delta_n$ requires $\sum_j q_j = 1$ . So $v_{\max}$ and $M$ are genuine maxima.
$n = 1$ :
- $q = (1)$ , $M = -\log 1 = 0$ , and $\Delta_1 = \{(1)\}$ with $D = 0$ there.
- Part (a) says $0$ is the greatest value of $D$ .
- Since $\beta > 0 \ge M$ , part (b) always applies: the set is $\{(1)\}$ and the greatest value of $\sum_j p_j v_j$ is $v_1 = v_{\max}$ .
$q$ uniform: every $q_i = 1/n$ , so $M = \log n$ .

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

§6.1, p. 791 — for β≥max⁡i(−log⁡qi)\beta\ge\max_i(-\log q_i)β≥maxi​(−logqi​) the entropy set is the whole simplex and the worst case is vmax⁡v_{\max}vmax​

§6.1, p. 791 — for $\beta\ge\max_i(-\log q_i)$ the entropy set is the whole simplex and the worst case is $v_{\max}$