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

condRuzsaDist_diff_ofsum_le

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:1433 to 1445

Mathematical statement

Exact Lean statement

lemma condRuzsaDist_diff_ofsum_le [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
    {X : Ω → G} {Y Z Z' : Ω' → G}
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (hZ' : Measurable Z')
    (h : iIndepFun ![Y, Z, Z'] μ')
    [FiniteRange X] [FiniteRange Z] [FiniteRange Y] [FiniteRange Z'] :
    d[X ; μ # Y + Z | Y + Z + Z'; μ'] - d[X ; μ # Y; μ'] ≤
    (H[Y + Z + Z'; μ'] + H[Y + Z; μ'] - H[Y ; μ'] - H[Z' ; μ'])/2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condRuzsaDist_diff_ofsum_le [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']    {X : Ω → G} {Y Z Z' : Ω' → G}    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (hZ' : Measurable Z')    (h : iIndepFun ![Y, Z, Z'] μ')    [FiniteRange X] [FiniteRange Z] [FiniteRange Y] [FiniteRange Z'] :    d[X ; μ # Y + Z | Y + Z + Z'; μ'] - d[X ; μ # Y; μ'] ≤    (H[Y + Z + Z'; μ'] + H[Y + Z; μ'] - H[Y ; μ'] - H[Z' ; μ'])/2 := by  have hadd : IndepFun (Y + Z) Z' μ' :=    (h.indepFun_add_left (Fin.cases hY <| Fin.cases hZ <| Fin.cases hZ' Fin.rec0) 0 1 2      (show 0 ≠ 2 by decide) (show 1 ≠ 2 by decide))  have h1 := condRuzsaDist_diff_le'' μ hX (show Measurable (Y + Z) by fun_prop) hZ' hadd  have h2 := condRuzsaDist_diff_le μ hX hY hZ (h.indepFun (show 0 ≠ 1 by decide))  linarith [h1, h2]