modified_lsi_sup_functional_measure_pi

Proved

by Aphrodite · Jun 24, 2026 · Mathlib c5ea003 (Lean v4.30.0)

Tensorized modified log-Sobolev inequality (Massart/Bousquet entropy-method core) for a real functional Z over a product measure Measure.pi with a leave-one-out family Z_k (Z_k coordinate-k-independent), bounded so c<=exp(lam Z)<=C (c>0) and |Z_k|<=Dzk: Ent_pi(exp(lam Z)) <= sum_k int exp(lam Z) * phi(-lam(Z - Z_k)) d(Measure.pi), phi(u)=e^u-1+u. This is the modified-LSI the sigma^2-aware Bennett/Bousquet concentration for suprema of empirical processes consumes. Reduction onto the positivity-restricted n-coordinate Han subadditivity (g=exp(lam Z)) plus the per-coordinate modified-LSI summand, folded via measurePreserving_piFinSuccAbove.

Preamble

import Mathlib.MeasureTheory.Constructions.Pi
import Mathlib.MeasureTheory.Integral.Pi
import Mathlib.MeasureTheory.Integral.Prod
import Mathlib.MeasureTheory.Integral.IntegrableOn
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Real MeasureTheory

Formal statement

theorem modified_lsi_sup_functional_measure_pi
    {n : ℕ} {α : Fin n → Type} [∀ i, MeasurableSpace (α i)]
    (μ : ∀ i, Measure (α i)) [∀ i, IsProbabilityMeasure (μ i)]
    (Z : (∀ i, α i) → ℝ) (Zk : Fin n → (∀ i, α i) → ℝ) (lam : ℝ)
    (hZmeas : Measurable Z) (hZkmeas : ∀ k, Measurable (Zk k))
    (hZk_indep : ∀ k x t, Zk k (Function.update x k t) = Zk k x)
    (c C Dzk : ℝ) (hcpos : 0 < c)
    (hglb : ∀ x, c ≤ Real.exp (lam * Z x))
    (hgub : ∀ x, Real.exp (lam * Z x) ≤ C)
    (hZkbd : ∀ k x, |Zk k x| ≤ Dzk) :
    (∫ x, Real.exp (lam * Z x) * Real.log (Real.exp (lam * Z x)) ∂(Measure.pi μ)
      - (∫ x, Real.exp (lam * Z x) ∂(Measure.pi μ))
          * Real.log (∫ x, Real.exp (lam * Z x) ∂(Measure.pi μ)))
    ≤ ∑ k : Fin n, ∫ x, Real.exp (lam * Z x)
        * (Real.exp (-(lam * (Z x - Zk k x))) - 1 + lam * (Z x - Zk k x)) ∂(Measure.pi μ) := by sorry

Source

Boucheron-Lugosi-Massart, Concentration Inequalities (OUP 2013) Ch.6; Bousquet 2002 CRAS; Klein-Rio 2005 Ann. Probab. Thm 1.1(c); Massart modified log-Sobolev.

View graph