Proposition 8 — the Bayesian optimal return f(i, g) is convex in the prior g

Proved

SatiaLave.Bayes.prop8_convex_in_prior

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

bayesian-mdpconvexitydynamic-programmingp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $f(i,g)$ be a bounded solution of the Bayesian recursive equations (10) of Satia and Lave (by Proposition 6 it is the unique one, the Bayesian optimal total expected discounted return). Let $g_1, g_2$ be priors on the unknown transition matrix and $0 \le t \le 1$ .

Proposition 8. $f(i, g)$ is convex in $g$ for any state $i$ :

f\big(i,\ t\, g_1 + (1-t)\, g_2\big) \le t\, f(i, g_1) + (1-t)\, f(i, g_2).

Convexity in the prior is what allows Jensen's inequality in the proof of Proposition 9.

Formalization Note The set of priors has no vector structure other than mixtures, so "convex in $g$ " is read as convexity along mixtures $t g_1 + (1-t) g_2$ of priors (measures). The proof is in Satia's thesis (reference 14 of the paper).

Preamble

import Mathlib
import Definitions.Def_SatiaLave_Bayes_Model

open MeasureTheory

Formal statement

namespace SatiaLave.Bayes

/-- Proposition 8: the Bayesian optimal return `f(i, g)` is convex in the prior `g`, along
mixtures `t g₁ + (1 - t) g₂` of priors. -/
theorem prop8_convex_in_prior {S : Type*} [Fintype S] [DecidableEq S] [Nonempty S]
    {D : S → Type*} [∀ i, Fintype (D i)] [∀ i, DecidableEq (D i)] [∀ i, Nonempty (D i)]
    (M : UncertainMDP S D)
    (f : S → Measure (Mat S D) → ℝ) (hf : SolvesEq10 M f) (hb : IsBoundedOnPriors f)
    (g₁ g₂ : Measure (Mat S D)) (hg₁ : IsPrior g₁) (hg₂ : IsPrior g₂)
    (t : ℝ) (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (i : S) :
    f i (ENNReal.ofReal t • g₁ + ENNReal.ofReal (1 - t) • g₂) ≤
      t * f i g₁ + (1 - t) * f i g₂ := by sorry

end SatiaLave.Bayes

Source

Satia and Lave, Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3), 1973, p. 735, Proposition 8

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting.

$S$ is a finite, nonempty set of states with decidable equality.
For each state $i$ , $D_i$ is a finite, nonempty set of decisions.
$M$ is an uncertain MDP: real rewards $r^k_{ij}$ , a discount $0\le\beta<1$ , and closed, convex, nonempty sets $U^k_i\subseteq\Delta_S$ .
$f:S\times\{\text{measures on }\mathcal M\}\to\mathbb R$ $f : S \times {measures on M} \to R$ satisfies two conditions:
- for every $i$ and every prior $g$ ,

f(i,g)=\max_{k\in D_i}\Big\{\sum_j\bar p^k_{ij}(g)\,r^k_{ij}+\beta\sum_j\bar p^k_{ij}(g)\,f(j,T^k_{ij}g)\Big\};

there is a real $C$ with $|f(i,g)|\le C$ for all $i$ and all priors $g$ .
Here $\bar p^k_{ij}(g)=\int p^k_{ij}\,dg$ .
$T^k_{ij}g$ is the measure with density $\max(p^k_{ij},0)/\bar p^k_{ij}(g)$ with respect to $g$ if $\bar p^k_{ij}(g)\neq0$ , and $g$ otherwise.
A prior is a probability measure on $\mathcal M$ that gives measure $0$ to the matrices with some row outside $\Delta_S$ .
$g_1,g_2$ are priors.
$t$ is a real number with $0\le t\le 1$ .
$i\in S$ is a state.

Claim.

f\big(i,\;t\,g_1+(1-t)\,g_2\big)\;\le\;t\,f(i,g_1)+(1-t)\,f(i,g_2).

The argument on the left is the mixture measure $A\mapsto t\,g_1(A)+(1-t)\,g_2(A)$ .

Degenerate cases.

At $t=1$ the mixture equals $g_1$ ; at $t=0$ it equals $g_2$ . In both cases the inequality reads $f(i,g)\le f(i,g)$ .
If $g_1=g_2$ , the inequality is again an equality.
The inequality is stated only along mixtures of two priors, at a fixed state $i$ .
The sets $U^k_i$ play no role.
The statement is conditional on $f$ satisfying both hypotheses. If no such $f$ exists, it holds vacuously.

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