Source indexedlemma · leanprover/lean4:v4.33.0-rc1

condRuzsaDist_le'_prod

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:1336 to 1349

Mathematical statement

Exact Lean statement

lemma condRuzsaDist_le'_prod [Countable T] {X : Ω → G} {Y : Ω' → G} {W Z : Ω' → T}
    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
    (hX : Measurable X) (hY : Measurable Y) (hW : Measurable W) (hZ : Measurable Z)
    [FiniteRange X] [FiniteRange Y] [FiniteRange W] [FiniteRange Z] :
    d[X ; μ # Y|⟨W, Z⟩ ; μ'] ≤ d[X ; μ # Y|Z ; μ'] + I[Y : W | Z ; μ']/2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condRuzsaDist_le'_prod [Countable T] {X : Ω → G} {Y : Ω' → G} {W Z : Ω' → T}    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']    (hX : Measurable X) (hY : Measurable Y) (hW : Measurable W) (hZ : Measurable Z)    [FiniteRange X] [FiniteRange Y] [FiniteRange W] [FiniteRange Z] :    d[X ; μ # Y|⟨W, Z⟩ ; μ'] ≤ d[X ; μ # Y|Z ; μ'] + I[Y : W | Z ; μ']/2 := by  rw [condRuzsaDist'_prod_eq_sum _ _ hY hW hZ, condRuzsaDist'_eq_sum hY hZ,    condMutualInfo_eq_sum hZ, Finset.sum_div, ← Finset.sum_add_distrib]  gcongr with z  rw [mul_div_assoc, ← mul_add]  rcases eq_or_ne (μ' (Z ⁻¹' {z})) 0 with hz | hz  · simp [measureReal_def, hz]  · have : IsProbabilityMeasure (μ'[|Z ⁻¹' {z}]) := cond_isProbabilityMeasure hz    gcongr    exact condRuzsaDist_le' _ _ hX hY hW