Eq. (48), p. 791 — $q^{\mathsf T}v+\beta\lambda\le\sigma(\lambda)\le v_{\max}+\beta\lambda$

Proved

RobustMDP.EntropyInner.dualFn_bounds

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

convex-dualitylog-sum-expp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $q\in\Delta_n$ with $q(j)>0$ for all $j$ , let $\beta>0$ and $v\in\mathbb R^n$ , and let $\sigma(\lambda)=\lambda\log\big(\sum_j q(j)e^{v(j)/\lambda}\big)+\beta\lambda$ be the dual function (47). Then for every $\lambda>0$ ,

q^{\mathsf T}v+\beta\lambda \;\le\; \sigma(\lambda) \;\le\; v_{\max}+\beta\lambda,

where $v_{\max}=\max_j v(j)$ .

The two affine bounds give the starting bracket of the bisection algorithm that minimises $\sigma$ .

Formalization Note The paper states (48) for all $\lambda\ge 0$ with the convention $\sigma(0)=v_{\max}$ . At $\lambda=0$ both inequalities then read $q^{\mathsf T}v\le v_{\max}\le v_{\max}$ , and the value $\sigma(0)=v_{\max}$ is the limit of Eq. (49) (a separate milestone). The statement here is for $\lambda>0$ , where $\sigma$ is given by formula (47).

Preamble

import Mathlib
import Definitions.Def_RobustMDP_EntropyInner_dualFunction

Formal statement

namespace RobustMDP.EntropyInner

/-- Eq. (48) (Nilim–El Ghaoui 2005, §6.3, p. 791; proof in Appendix C, p. 797). For `q ∈ Δₙ` with
`q > 0`, `β > 0` and every `λ > 0`,
`qᵀv + β λ ≤ σ(λ) ≤ v_max + β λ`, where `σ` is the dual function (47). -/
theorem dualFn_bounds {n : ℕ} (q v : Fin n → ℝ) (β : ℝ)
    (hq : q ∈ stdSimplex ℝ (Fin n)) (hq_pos : ∀ j, 0 < q j) (hβ : 0 < β) :
    ∀ lam : ℝ, 0 < lam →
      (∑ j, q j * v j) + β * lam ≤ dualFn q v β lam ∧
      dualFn q v β lam ≤ vmax v + β * lam := 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.3, Eq. (48); proof in Appendix C, p. 797

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: $q_j \ge 0$ and $\sum_j q_j = 1$ ;
$q_j > 0$ for every $j$ ;
$\beta > 0$ .

Notation.

The dual function is

\sigma(\lambda) = \lambda \log\!\Big(\sum_j q_j e^{v_j/\lambda}\Big) + \beta\lambda .

For $\lambda > 0$ the sum inside the logarithm is strictly positive, so this is the ordinary logarithm.

$v_{\max} = \max_j v_j$ , the supremum of the coordinates of $v$ .

Conclusion. For every real $\lambda > 0$ ,

\sum_j q_j v_j + \beta\lambda \;\le\; \sigma(\lambda) \;\le\; v_{\max} + \beta\lambda .

Both inequalities are non-strict. Nothing is asserted for $\lambda \le 0$ .

Degenerate cases.

$n = 0$ : excluded by the simplex hypothesis, so $v_{\max}$ is a genuine maximum.
$n = 1$ : $q = (1)$ and $\sigma(\lambda) = v_1 + \beta\lambda$ . Both inequalities are equalities.
$v$ constant, all $v_j = c$ : $\sigma(\lambda) = c + \beta\lambda$ , and again both sides are equalities.
$\lambda = 0$ : the value there, which by the division convention would be $0$ , is not covered.

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

Eq. (48), p. 791 — qTv+βλ≤σ(λ)≤vmax⁡+βλq^{\mathsf T}v+\beta\lambda\le\sigma(\lambda)\le v_{\max}+\beta\lambdaqTv+βλ≤σ(λ)≤vmax​+βλ

Eq. (48), p. 791 — $q^{\mathsf T}v+\beta\lambda\le\sigma(\lambda)\le v_{\max}+\beta\lambda$