entropy_n_coordinate_han_subadditivity_measure_pi_pos

Proved

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

N-coordinate Han entropy subadditivity (tensorization) over a product measure Measure.pi, positivity-restricted form: for probability measures mu_i and a measurable g with 0<cc<=g<=CC, Ent_pi(g) <= sum_k [ int g log g - int (int_t g(update x k t) dmu_k) log(...) ]. BLM Concentration Inequalities Ch.4 Thm 4.10 / Ch.6 entropy method. Proven by induction on n from the TRUE positivity-restricted 2-coordinate Han (chain rule + convexity refinement). The positivity hypothesis is essential; the unconditional 2-coord Han over arbitrary real F is FALSE.

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 entropy_n_coordinate_han_subadditivity_measure_pi_pos :
    ∀ {n : ℕ} {α : Fin n → Type} [∀ i, MeasurableSpace (α i)]
    (μ : ∀ i, Measure (α i)) [∀ i, IsProbabilityMeasure (μ i)]
    (g : (∀ i, α i) → ℝ) (cc CC : ℝ), 0 < cc →
    Measurable g → (∀ x, cc ≤ g x) → (∀ x, g x ≤ CC) →
    ((∫ x, g x * Real.log (g x) ∂(Measure.pi μ))
        - (∫ x, g x ∂(Measure.pi μ)) * Real.log (∫ x, g x ∂(Measure.pi μ)))
      ≤ ∑ k : Fin n,
          ((∫ x, g x * Real.log (g x) ∂(Measure.pi μ))
            - ∫ x, (∫ t, g (Function.update x k t) ∂(μ k))
                * Real.log (∫ t, g (Function.update x k t) ∂(μ k)) ∂(Measure.pi μ)) := by sorry

Source

Boucheron-Lugosi-Massart, Concentration Inequalities (OUP 2013), Ch.4 Thm 4.10 / Ch.6 entropy method.

View graph