§6.3, p. 792 — if $\beta\ge-\log Q(v)$ then $\lambda=0$ is optimal and the value is $v_{\max}$

Proved

RobustMDP.EntropyInner.lambda_zero_optimal

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

convex-dualityp2o-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$ , and let $\sigma$ be the dual function (47), $v_{\max}=\max_j v(j)$ and $Q(v)=\sum_{j:\,v(j)=v_{\max}}q(j)$ . If

\beta \;\ge\; -\log Q(v)

(equivalently $\sigma'(0)=\beta+\log Q(v)\ge 0$ ), then

$\inf_{\lambda>0}\sigma(\lambda)=v_{\max}$ , so $\lambda=0$ is optimal for the dual;
the worst-case value of $p^{\mathsf T}v$ over $\mathcal P=\{p\in\Delta_n : D(p\|q)\le\beta\}$ is $v_{\max}$ , and it is attained.

For such $\beta$ robustness disregards the prior information carried by $q$ . Unlike the threshold $\max_i(-\log q_i)$ of §6.1, the threshold $-\log Q(v)$ depends on $v$ .

Formalization Note The infimum is stated with IsGLB over $\{\sigma(\lambda):\lambda>0\}$ ; it is not attained at any $\lambda>0$ in general, which is why the paper speaks of $\lambda=0$ . The paper's first sentence has the non-strict condition $\sigma'(0)\ge 0$ and its second sentence the strict $\beta>-\log Q(v)$ ; the statement here uses the non-strict version, which contains both.

Preamble

import Mathlib
import Definitions.Def_RobustMDP_EntropyInner_klBall
import Definitions.Def_RobustMDP_EntropyInner_dualFunction

Formal statement

namespace RobustMDP.EntropyInner

/-- §6.3 (Nilim–El Ghaoui 2005, p. 792). For `q ∈ Δₙ` with `q > 0` and `β > 0`: if
`β ≥ −log Q(v)` (equivalently `σ'(0) = β + log Q(v) ≥ 0`), then `λ = 0` is optimal for the dual:
the infimum of `σ` over `λ > 0` is `v_max`, and the worst-case value of `pᵀv` over the entropy set
`𝒫 = {p ∈ Δₙ : D(p‖q) ≤ β}` is `v_max` (attained). -/
theorem lambda_zero_optimal {n : ℕ} (q v : Fin n → ℝ) (β : ℝ)
    (hq : q ∈ stdSimplex ℝ (Fin n)) (hq_pos : ∀ j, 0 < q j) (hβ : 0 < β)
    (hβQ : -Real.log (maxMass q v) ≤ β) :
    IsGLB ((fun lam => dualFn q v β lam) '' Set.Ioi 0) (vmax v) ∧
    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. 792, §6.3, second 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$ lies in the probability simplex $\Delta_n$ ( $q_j \ge 0$ , $\sum_j q_j = 1$ );
$q_j > 0$ for every $j$ ;
$\beta > 0$ ;
$-\log Q(v) \le \beta$ .

Notation.

$v_{\max} = \max_j v_j$ .
$Q(v) = \sum_{j : v_j = v_{\max}} q_j$ . Under the hypotheses $0 < Q(v) \le 1$ , so $-\log Q(v) \ge 0$ is an ordinary logarithm.
The dual function is $\sigma(\lambda) = \lambda \log\big(\sum_j q_j e^{v_j/\lambda}\big) + \beta\lambda$ .
$D(p\,\|\,q) = \sum_j p_j\log(p_j/q_j)$ , where a term with $p_j = 0$ contributes $0$ .
$\mathcal{B}(q,\beta) = \{p \in \Delta_n : D(p\,\|\,q) \le \beta\}$ .

Conclusion (dual). $v_{\max}$ is the greatest lower bound of $\{\sigma(\lambda) : \lambda > 0\}$ . That is:

$\sigma(\lambda) \ge v_{\max}$ for every $\lambda > 0$ ;
no larger number is a lower bound.

It is not asserted that some $\lambda > 0$ attains $v_{\max}$ .

Conclusion (worst case). $v_{\max}$ is the greatest element of $\{\sum_j p_j v_j : p \in \mathcal{B}(q,\beta)\}$ . That is:

$\sum_j p_j v_j \le v_{\max}$ for every $p \in \mathcal{B}(q,\beta)$ ;
equality holds for some $p \in \mathcal{B}(q,\beta)$ .

Degenerate cases.

$n = 0$ : excluded by the simplex hypothesis.
$n = 1$ , or $v$ constant:
- $Q(v) = 1$ , so the last hypothesis reduces to $0 \le \beta$ , which $\beta > 0$ already implies.
- $\sigma(\lambda) = v_{\max} + \beta\lambda$ , whose infimum over $\lambda > 0$ is $v_{\max}$ and is not attained.
Unique maximiser $j_0$ : the hypothesis becomes $\beta \ge -\log q_{j_0}$ .

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.3, p. 792 — if β≥−log⁡Q(v)\beta\ge-\log Q(v)β≥−logQ(v) then λ=0\lambda=0λ=0 is optimal and the value is vmax⁡v_{\max}vmax​

§6.3, p. 792 — if $\beta\ge-\log Q(v)$ then $\lambda=0$ is optimal and the value is $v_{\max}$