kaimanovich_vershik

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  have : IsProbabilityMeasure μ := h.isProbabilityMeasure  suffices (H[X ; μ] + H[Y ; μ] + H[Z ; μ]) + H[X + Y + Z ; μ]    ≤ (H[X ; μ] + H[Y + Z ; μ]) + (H[Z ; μ] + H[X + Y ; μ]) by linarith  have : ∀ (i : Fin 3), Measurable (![X, Y, Z] i) := fun i ↦ by fin_cases i <;> assumption  convert entropy_triple_add_entropy_le μ hX hZ (show Measurable (X + (Y + Z)) by fun_prop)    using 2  · calc      H[X ; μ] + H[Y ; μ] + H[Z ; μ] = H[⟨X, Y⟩ ; μ] + H[Z ; μ] := by        rw [IndepFun.entropy_pair_eq_add hX hY]        exact h.indepFun (show 0 ≠ 1 by decide)      _ = H[⟨⟨X, Y⟩, Z⟩ ; μ] := by        rw [IndepFun.entropy_pair_eq_add (hX.prodMk hY) hZ]        exact h.indepFun_prodMk this 0 1 2 (by decide) (by decide)      _ = H[⟨X, ⟨Z , X + (Y + Z)⟩⟩ ; μ] := by        apply entropy_of_comp_eq_of_comp μ (by fun_prop) (by fun_prop)          (fun ((x, y), z) ↦ (x, z, x + y + z)) (fun (a, b, c) ↦ ((a, c - a - b), b))        all_goals { funext ω; dsimp [prod]; ext <;> dsimp; abel }  · rw [add_assoc]  · symm    refine (entropy_add_right hX (by fun_prop) _).trans <|      IndepFun.entropy_pair_eq_add hX (by fun_prop) ?_    exact h.indepFun_add_right this 0 1 2 (by decide) (by decide)  · rw [eq_comm, ← add_assoc]    refine (entropy_add_right' hZ (by fun_prop) _).trans <|      IndepFun.entropy_pair_eq_add hZ (by fun_prop) ?_    exact h.indepFun_add_right this 2 0 1 (by decide) (by decide)