Scalar conditional entropy decreases under refinement

Proved

OnlineNRM.TSFixed.finitePosteriorEntropy_scalar_mono

by Eyal1990 · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

banditsp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1revenue-managementthompson-sampling

For a measurable [0,1]-valued scalar function, expected entropy of its conditional mean decreases when the conditioning σ-algebra is refined, including when either conditioning σ-algebra is outside the ambient one under Mathlib’s zero convention.

Preamble

import Definitions.Def_OnlineNRM_TSFixed_OracleEntropy

open MeasureTheory ProbabilityTheory
open scoped BigOperators

Formal statement

theorem OnlineNRM.TSFixed.finitePosteriorEntropy_scalar_mono
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P]
    (m₁ m₂ : MeasurableSpace Ω) (hm : m₁ ≤ m₂)
    (f : Ω → ℝ)
    (hfmeas : @Measurable Ω ℝ mΩ inferInstance f)
    (hf0 : ∀ ω, 0 ≤ f ω)
    (hf1 : ∀ ω, f ω ≤ 1) :
    ∫ ω, Real.negMulLog ((P[fun ω' => f ω' | m₂]) ω) ∂P ≤
      ∫ ω, Real.negMulLog ((P[fun ω' => f ω' | m₁]) ω) ∂P := by sorry

Source

Ferreira, Simchi-Levi, Wang, Online Network Revenue Management Using Thompson Sampling, Oper. Res. 66(6), 2018, p. 1594, Theorem 1

View graph