Eq. (49), p. 791 — $\sigma(\lambda)=v_{\max}+(\beta+\log Q(v))\lambda+o(\lambda)$ as $\lambda\to0^+$

Proved

RobustMDP.EntropyInner.dualFn_at_zero

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

asymptoticslog-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$ be the dual function (47). Write $v_{\max}=\max_j v(j)$ and $Q(v)=\sum_{j:\,v(j)=v_{\max}}q(j)$ . Then, as $\lambda\to 0^+$ ,

\sigma(\lambda)=v_{\max}+(\beta+\log Q(v))\lambda+o(\lambda).

In particular $\sigma(\lambda)\to v_{\max}$ , which is the paper's $\sigma(0)=v_{\max}$ , and the right derivative of $\sigma$ at $0$ is $\sigma'(0)=\beta+\log Q(v)$ .

The expansion at $0$ decides whether the minimum of $\sigma$ is attained at an interior $\lambda$ or only in the limit $\lambda\to0^+$ .

Formalization Note The statement has two parts: Tendsto of $\sigma$ to $v_{\max}$ along 𝓝[>] 0, and the remainder $\sigma(\lambda)-v_{\max}-(\beta+\log Q(v))\lambda$ is little-o of $\lambda$ along 𝓝[>] 0. Appendix C in fact shows the remainder is $O(\lambda e^{-t/\lambda})$ for some $t>0$ ; the statement here is the printed $o(\lambda)$ .

Preamble

import Mathlib
import Definitions.Def_RobustMDP_EntropyInner_dualFunction
open Filter Topology

Formal statement

namespace RobustMDP.EntropyInner

/-- Eq. (49) (Nilim–El Ghaoui 2005, §6.3, p. 791; proof in Appendix C, p. 797). For `q ∈ Δₙ` with
`q > 0` and `β > 0`, as `λ → 0⁺`,
`σ(λ) = v_max + (β + log Q(v)) λ + o(λ)`, where `Q(v) = ∑_{j : v(j) = v_max} q(j)`. In particular
`σ(λ) → v_max` (the paper's `σ(0) = v_max`). -/
theorem dualFn_at_zero {n : ℕ} (q v : Fin n → ℝ) (β : ℝ)
    (hq : q ∈ stdSimplex ℝ (Fin n)) (hq_pos : ∀ j, 0 < q j) (hβ : 0 < β) :
    Tendsto (fun lam => dualFn q v β lam) (𝓝[>] 0) (𝓝 (vmax v)) ∧
    (fun lam => dualFn q v β lam - vmax v - (β + Real.log (maxMass q v)) * lam)
      =o[𝓝[>] 0] (fun lam : ℝ => 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. (49) and the definition of Q(v); 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$ , $\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$ .
$v_{\max} = \max_j v_j$ , the supremum of the coordinates of $v$ .
The mass at the maximum is

Q(v) = \sum_{j : v_j = v_{\max}} q_j .

Under the hypotheses, $0 < Q(v) \le 1$ , so $\log Q(v) \le 0$ is an ordinary logarithm.

Conclusion (limit). As $\lambda \to 0$ from the right, meaning through values $\lambda > 0$ ,

\sigma(\lambda) \to v_{\max}.

Conclusion (first-order behaviour). As $\lambda \to 0^{+}$ ,

\sigma(\lambda) - v_{\max} - \big(\beta + \log Q(v)\big)\lambda \;=\; o(\lambda).

That is, for every $\varepsilon > 0$ there is a $\delta > 0$ such that the absolute value of the left side is at most $\varepsilon\lambda$ whenever $0 < \lambda < \delta$ .

The statement is only about $\lambda > 0$ near $0$ . It says nothing about the value at $\lambda = 0$ itself, which by the division convention would be $0$ .

Degenerate cases.

$n = 0$ : excluded by the simplex hypothesis.
$n = 1$ , or $v$ constant:
- $Q(v) = 1$ and $\log Q(v) = 0$ .
- $\sigma(\lambda) = v_{\max} + \beta\lambda$ exactly, so both claims hold trivially.
Unique maximising coordinate $j_0$ : $Q(v) = 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

Eq. (49), p. 791 — σ(λ)=vmax⁡+(β+log⁡Q(v))λ+o(λ)\sigma(\lambda)=v_{\max}+(\beta+\log Q(v))\lambda+o(\lambda)σ(λ)=vmax​+(β+logQ(v))λ+o(λ) as λ→0+\lambda\to0^+λ→0+

Eq. (49), p. 791 — $\sigma(\lambda)=v_{\max}+(\beta+\log Q(v))\lambda+o(\lambda)$ as $\lambda\to0^+$