§6.2, p. 791 — eliminating $\mu$ : $\min_\mu d(\lambda,\mu)=\sigma(\lambda)$ of (47)

Proved

RobustMDP.EntropyInner.mu_elimination

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$ , $v\in\mathbb R^n$ and $\lambda>0$ . Consider the two-variable dual objective

d(\lambda,\mu)=\mu+\beta\lambda+\lambda\sum_j q(j)\exp\Big(\frac{v(j)-\mu}{\lambda}-1\Big),\qquad \mu\in\mathbb R,

and put $\mu^*=\lambda\log\big(\sum_j q(j)\exp(v(j)/\lambda)\big)-\lambda$ . Then

$\mu^*$ satisfies the optimality condition $\sum_j q(j)\exp\big(\frac{v(j)-\mu^*}{\lambda}-1\big)=1$ ;
$d(\lambda,\mu^*)=\sigma(\lambda)$ , where $\sigma(\lambda)=\lambda\log\big(\sum_j q(j)e^{v(j)/\lambda}\big)+\beta\lambda$ is the function (47);
$\sigma(\lambda)$ is the minimum of $d(\lambda,\cdot)$ over $\mu\in\mathbb R$ :

\min_{\mu\in\mathbb R} d(\lambda,\mu)=\sigma(\lambda).

This reduces the two-variable dual $\min_{\lambda>0,\mu} d(\lambda,\mu)$ of the inner problem to the one-dimensional problem $\min_{\lambda>0}\sigma(\lambda)$ .

Formalization Note The minimum over $\mu$ is stated with IsLeast on the range of $\mu\mapsto d(\lambda,\mu)$ , so it is both a lower bound and attained.

Preamble

import Mathlib
import Definitions.Def_RobustMDP_EntropyInner_dualFunction

Formal statement

namespace RobustMDP.EntropyInner

/-- Elimination of `μ` in the dual of §6.2 (Nilim–El Ghaoui 2005, p. 791). For `q ∈ Δₙ` with
`q > 0`, `β > 0` and `λ > 0`, put `μ* = λ log (∑ⱼ q(j) exp (v(j)/λ)) − λ`. Then `μ*` satisfies
the optimality condition `∑ⱼ q(j) exp ((v(j) − μ*)/λ − 1) = 1`, and the minimum over `μ ∈ ℝ` of the
two-variable dual objective `d(λ, μ) = μ + βλ + λ ∑ⱼ q(j) exp ((v(j) − μ)/λ − 1)` equals `σ(λ)` of
(47) and is attained at `μ*`. -/
theorem mu_elimination {n : ℕ} (q v : Fin n → ℝ) (β : ℝ)
    (hq : q ∈ stdSimplex ℝ (Fin n)) (hq_pos : ∀ j, 0 < q j) (hβ : 0 < β)
    (lam : ℝ) (hlam : 0 < lam) :
    (∑ j, q j * Real.exp
        ((v j - (lam * Real.log (∑ i, q i * Real.exp (v i / lam)) - lam)) / lam - 1)) = 1 ∧
    dualObj q v β lam (lam * Real.log (∑ i, q i * Real.exp (v i / lam)) - lam) =
        dualFn q v β lam ∧
    IsLeast (Set.range (fun mu : ℝ => dualObj q v β lam mu)) (dualFn q 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.2, from "Setting the derivative with respect to μ to zero" to Eq. (47)

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, \lambda \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$ ;
$\lambda > 0$ .

Notation.

$S = \sum_i q_i e^{v_i/\lambda}$ , which is strictly positive.
$\mu^{*} = \lambda \log S - \lambda$ .
The two-variable objective is

d(\lambda,\mu) = \mu + \beta\lambda + \lambda \sum_j q_j \exp\!\Big(\frac{v_j-\mu}{\lambda} - 1\Big).

The dual function is $\sigma(\lambda) = \lambda \log S + \beta\lambda$ .

Conclusion. Three facts hold:

The optimality equation holds at $\mu^{*}$ :

\sum_j q_j \exp\!\Big(\frac{v_j - \mu^{*}}{\lambda} - 1\Big) = 1 .

The objective at $\mu^{*}$ equals the dual function: $d(\lambda,\mu^{*}) = \sigma(\lambda)$ .
$\sigma(\lambda)$ $σ (λ)$ is the least element of $\{d(\lambda,\mu) : \mu \in \mathbb{R}\}$ ${d (λ, μ) : μ \in R}$ . That is:
- $d(\lambda,\mu) \ge \sigma(\lambda)$ for every real $\mu$ ;
- some real $\mu$ achieves $d(\lambda,\mu) = \sigma(\lambda)$ . By item 2, $\mu^{*}$ is one such value.

Uniqueness of the minimiser is not asserted.

Degenerate cases.

$n = 0$ : excluded by the simplex hypothesis.
$n = 1$ :
- $q = (1)$ , $S = e^{v_1/\lambda}$ and $\mu^{*} = v_1 - \lambda$ .
- The claims reduce to $e^{0} = 1$ and to $\min_\mu d(\lambda,\mu) = v_1 + \beta\lambda$ .
$\beta$ : it enters only as the additive constant $\beta\lambda$ on both sides. Its positivity is assumed but plays no visible role in the equations.
$\lambda \le 0$ : 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

§6.2, p. 791 — eliminating μ\muμ: min⁡μd(λ,μ)=σ(λ)\min_\mu d(\lambda,\mu)=\sigma(\lambda)minμ​d(λ,μ)=σ(λ) of (47)

§6.2, p. 791 — eliminating $\mu$ : $\min_\mu d(\lambda,\mu)=\sigma(\lambda)$ of (47)