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

kaimanovich_vershik'

PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:1146 to 1158

Source documentation

A version of the Kaimanovich-Vershik inequality with some variables negated.

Exact Lean statement

lemma kaimanovich_vershik' {X Y Z : Ω → G} (h : iIndepFun ![X, Y, Z] μ)
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    [FiniteRange X] [FiniteRange Z] [FiniteRange Y] :
    H[X - (Y + Z) ; μ] - H[X - Y ; μ] ≤ H[Y + Z ; μ] - H[Y ; μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma kaimanovich_vershik' {X Y Z : Ω → G} (h : iIndepFun ![X, Y, Z] μ)    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)    [FiniteRange X] [FiniteRange Z] [FiniteRange Y] :    H[X - (Y + Z) ; μ] - H[X - Y ; μ] ≤ H[Y + Z ; μ] - H[Y ; μ] := by  rw [← entropy_neg (X := Y + Z) (by fun_prop), ← entropy_neg hY]  simp_rw [sub_eq_add_neg, neg_add, ← add_assoc]  refine kaimanovich_vershik ?_ hX hY.neg hZ.neg  convert (h.neg 1).neg 2  ext i; fin_cases i  · simp (discharger := decide)  · simp (discharger := decide)  · rw [← show ∀ h : 2 < 3, (2 : Fin 3) = ⟨2, h⟩ by intro; rfl]    simp (discharger := decide)