Entropy integral bounds for measurable finite simplex vectors

Proved

ProbabilityTheory.integral_simplex_entropy_bounds

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 finite probability vector almost everywhere under a probability measure, the integral of the sum of coordinate entropies lies between zero and the logarithm of the number of coordinates. The pointwise entropy inequalities include the singleton case; integrating them requires showing the entropy integrand is integrable.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.Data.Fintype.BigOperators

open MeasureTheory
open scoped BigOperators

Formal statement

theorem ProbabilityTheory.integral_simplex_entropy_bounds
    {Ω α : Type*} [MeasurableSpace Ω] [Fintype α] [Nonempty α]
    (P : Measure Ω) [IsProbabilityMeasure P]
    (q : Ω → α → ℝ)
    (hqMeas : ∀ a, Measurable (fun ω => q ω a))
    (hq0 : ∀ᵐ ω ∂P, ∀ a, 0 ≤ q ω a)
    (hq1 : ∀ᵐ ω ∂P, ∑ a : α, q ω a = 1) :
    0 ≤ MeasureTheory.integral P (fun ω => ∑ a : α, Real.negMulLog (q ω a)) ∧
      MeasureTheory.integral P (fun ω => ∑ a : α, Real.negMulLog (q ω a)) ≤
        Real.log (Fintype.card α : ℝ) := 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