§6.2, p. 791 — the optimal distribution $p^*\propto q(j)e^{v(j)/\lambda}$ (Gibbs variational principle)

Proved

RobustMDP.EntropyInner.tilted_optimal

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

convex-dualitygibbs-variational-principlekullback-leibler-divergencep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $q\in\Delta_n$ with $q(j)>0$ for all $j$ , let $v\in\mathbb R^n$ and $\lambda>0$ .

For every $p\in\Delta_n$ ,

p^{\mathsf T}v-\lambda D(p\|q) \;\le\; \lambda\log\Big(\sum_j q(j)\exp\frac{v(j)}{\lambda}\Big).

The tilted distribution

p^*(j)=\frac{q(j)\exp(v(j)/\lambda)}{\sum_i q(i)\exp(v(i)/\lambda)}

belongs to $\Delta_n$ and attains equality in 1.

In words, $p^*$ maximises the penalised objective $p^{\mathsf T}v-\lambda D(p\|q)$ over the simplex, and the maximum is $\lambda$ times the log-moment-generating function of $v$ under $q$ at $1/\lambda$ . This is what makes $p^*$ the optimal distribution for a given multiplier $\lambda$ in the dual of the inner problem.

Formalization Note The paper only displays the formula for $p^*$ ("The optimal distribution is"); the inequality in 1 with equality at $p^*$ is the content that display relies on.

Preamble

import Mathlib
import Definitions.Def_RobustMDP_EntropyInner_klBall
import Definitions.Def_RobustMDP_EntropyInner_dualFunction

Formal statement

namespace RobustMDP.EntropyInner

/-- The optimal distribution of §6.2 (Nilim–El Ghaoui 2005, p. 791), in variational form.
For `q ∈ Δₙ` with `q > 0` and `λ > 0`:
(a) every `p ∈ Δₙ` satisfies `pᵀv − λ D(p‖q) ≤ λ log ∑ⱼ q(j) exp (v(j)/λ)`;
(b) the tilted distribution `p*(j) = q(j) exp (v(j)/λ) / ∑ᵢ q(i) exp (v(i)/λ)` lies in `Δₙ` and
attains equality in (a). -/
theorem tilted_optimal {n : ℕ} (q v : Fin n → ℝ)
    (hq : q ∈ stdSimplex ℝ (Fin n)) (hq_pos : ∀ j, 0 < q j) (lam : ℝ) (hlam : 0 < lam) :
    (∀ p ∈ stdSimplex ℝ (Fin n),
      (∑ j, p j * v j) - lam * klDiv p q ≤
        lam * Real.log (∑ j, q j * Real.exp (v j / lam))) ∧
    tiltedDist q v lam ∈ stdSimplex ℝ (Fin n) ∧
    (∑ j, tiltedDist q v lam j * v j) - lam * klDiv (tiltedDist q v lam) q =
        lam * Real.log (∑ j, q j * Real.exp (v j / 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, display "The optimal distribution is p* = …"

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 $\lambda \in \mathbb{R}$ . Assume:

$q$ lies in the probability simplex $\Delta_n = \{p : p_j \ge 0,\ \sum_j p_j = 1\}$ ;
$q_j > 0$ for every $j$ ;
$\lambda > 0$ .

No $\beta$ appears.

Notation.

$D(p\,\|\,q) = \sum_j p_j \log(p_j/q_j)$ , where a term with $p_j = 0$ contributes $0$ .
$S = \sum_j q_j e^{v_j/\lambda}$ , which is strictly positive.
$p^{*}_j = q_j e^{v_j/\lambda} / S$ .

Conclusion (a). For every $p \in \Delta_n$ ,

\sum_j p_j v_j \;-\; \lambda\, D(p\,\|\,q) \;\le\; \lambda \log S .

Conclusion (b). $p^{*} \in \Delta_n$ .

Conclusion (c). Equality holds at $p^{*}$ :

\sum_j p^{*}_j v_j \;-\; \lambda\, D(p^{*}\,\|\,q) \;=\; \lambda \log S .

Degenerate cases.

$n = 0$ : impossible, because of the simplex hypothesis on $q$ .
$n = 1$ :
- $q = p^{*} = (1)$ , $D = 0$ and $\lambda\log S = v_1$ .
- Parts (a) and (c) both reduce to $v_1 \le v_1$ and $v_1 = v_1$ .
Zero coordinates of $p$ : for $p \in \Delta_n$ with some $p_j = 0$ , those coordinates contribute nothing to $D$ , which matches the convention $0\log 0 = 0$ .
$\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 — the optimal distribution p∗∝q(j)ev(j)/λp^*\propto q(j)e^{v(j)/\lambda}p∗∝q(j)ev(j)/λ (Gibbs variational principle)

§6.2, p. 791 — the optimal distribution $p^*\propto q(j)e^{v(j)/\lambda}$ (Gibbs variational principle)