Eq. (50), p. 791 — $\sigma(\lambda)=q^{\mathsf T}v+\beta\lambda+o(1)$ as $\lambda\to\infty$

Proved

RobustMDP.EntropyInner.dualFn_at_top

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). Then

\sigma(\lambda)=q^{\mathsf T}v+\beta\lambda+o(1)\qquad(\lambda\to\infty),

that is, $\sigma(\lambda)-(q^{\mathsf T}v+\beta\lambda)\to 0$ .

Together with the lower bound in (48), this says the affine function $q^{\mathsf T}v+\beta\lambda$ is the asymptote of $\sigma$ at infinity.

Preamble

import Mathlib
import Definitions.Def_RobustMDP_EntropyInner_dualFunction
open Filter Topology

Formal statement

namespace RobustMDP.EntropyInner

/-- Eq. (50) (Nilim–El Ghaoui 2005, §6.3, p. 791; proof in Appendix C, p. 797). For `q ∈ Δₙ` with
`q > 0` and `β > 0`, as `λ → ∞`, `σ(λ) = qᵀv + βλ + o(1)`. -/
theorem dualFn_at_top {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 - ((∑ j, q j * v j) + β * lam)) atTop (𝓝 0) := 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. (50); 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 .

Conclusion. As $\lambda \to +\infty$ ,

\sigma(\lambda) - \Big(\sum_j q_j v_j + \beta\lambda\Big) \;\longrightarrow\; 0 .

Equivalently, $\sigma(\lambda) = \sum_j q_j v_j + \beta\lambda + o(1)$ .

Degenerate cases.

$n = 0$ : excluded by the simplex hypothesis.
$n = 1$ , or $v$ constant: the difference is identically $0$ for $\lambda > 0$ .
$\beta$ : it cancels from the difference, so the hypothesis $\beta > 0$ plays no visible role.
Other values of $\lambda$ : only the behaviour for large positive $\lambda$ is asserted.

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. (50), p. 791 — σ(λ)=qTv+βλ+o(1)\sigma(\lambda)=q^{\mathsf T}v+\beta\lambda+o(1)σ(λ)=qTv+βλ+o(1) as λ→∞\lambda\to\inftyλ→∞

Eq. (50), p. 791 — $\sigma(\lambda)=q^{\mathsf T}v+\beta\lambda+o(1)$ as $\lambda\to\infty$