rdist_triangle

lemma rdist_triangle {X : Ω → G} {Y : Ω' → G} {Z : Ω'' → G}    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)    [hμ : IsProbabilityMeasure μ] [hμ' : IsProbabilityMeasure μ']    [hμ'' : IsProbabilityMeasure μ''] [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :    d[X ; μ # Z ; μ''] ≤ d[X ; μ # Y ; μ'] + d[Y ; μ' # Z ; μ''] := by  obtain ⟨A, mA, μA, X', Y', Z', hμA, hInd, hX', hY', hZ', HX, HY, HZ, _, _, _⟩ :=    independent_copies3_nondep_finiteRange hX hY hZ μ μ' μ''  suffices d[X' ; μA # Z' ; μA] ≤ d[X' ; μA # Y' ; μA] + d[Y' ; μA # Z' ; μA] by    rwa [HX.rdist_congr HY, HY.rdist_congr HZ, HX.rdist_congr HZ] at this  have IndepLem : IndepFun (⟨X', Z'⟩) Y' μA :=    iIndepFun.indepFun_prodMk hInd (fun i => by fin_cases i ; all_goals { simpa }) 0 2 1      (by norm_cast) (by norm_cast)  calc d[X' ; μA # Z' ; μA] = H[X' - Z'; μA] - (H[X'; μA] / 2 + H[Z'; μA] / 2) := by        rw [ProbabilityTheory.IndepFun.rdist_eq          (by simpa using hInd.indepFun (show 0 ≠ 2 by norm_cast)) hX' hZ'] ; ring    _ ≤ (H[X' - Y' ; μA] + H[Y' - Z' ; μA] - H[Y' ; μA]) - (H[X'; μA] / 2 + H[Z'; μA] / 2) :=          sub_le_sub_right (ent_of_diff_le _ _ _ hX' hZ' hY' IndepLem) _    _ = (H[X' - Y' ; μA] - H[X'; μA] / 2 - H[Y' ; μA] / 2) +          (H[Y' - Z' ; μA] - H[Y' ; μA] / 2 - H[Z'; μA] / 2) := by ring    _ = d[X' ; μA # Y' ; μA] + d[Y' ; μA # Z' ; μA] := by        rw [ProbabilityTheory.IndepFun.rdist_eq (by simpa using (iIndepFun.indepFun hInd          (show 0 ≠ 1 by norm_cast))) hX' hY', ProbabilityTheory.IndepFun.rdist_eq          (by simpa using (iIndepFun.indepFun hInd (show 1 ≠ 2 by norm_cast))) hY' hZ']