condRuzsaDist_le

lemma condRuzsaDist_le [Countable T] {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : Ω' → T}    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']    (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W)    [FiniteRange X] [FiniteRange Z] [FiniteRange Y] [FiniteRange W] :      d[X | Z ; μ # Y|W ; μ'] ≤ d[X ; μ # Y ; μ'] + I[X : Z ; μ]/2 + I[Y : W ; μ']/2 := by  have hXZ : Measurable (⟨X, Z⟩ : Ω → G × S):= hX.prodMk hZ  have hYW : Measurable (⟨Y, W⟩ : Ω' → G × T):= hY.prodMk hW  obtain ⟨ν, XZ', YW', _, hXZ', hYW', hind, hIdXZ, hIdYW, _, _⟩ :=    independent_copies_finiteRange hXZ hYW μ μ'  let X' := Prod.fst ∘ XZ'  let Z' := Prod.snd ∘ XZ'  let Y' := Prod.fst ∘ YW'  let W' := Prod.snd ∘ YW'  have hX' : Measurable X' := hXZ'.fst  have hZ' : Measurable Z' := hXZ'.snd  have hY' : Measurable Y' := hYW'.fst  have hW' : Measurable W' := hYW'.snd  have : FiniteRange W' := instFiniteRangeComp ..  have : FiniteRange X' := instFiniteRangeComp ..  have : FiniteRange Y' := instFiniteRangeComp ..  have : FiniteRange Z' := instFiniteRangeComp ..  have hind' : IndepFun X' Y' ν := hind.comp measurable_fst measurable_fst  rw [show XZ' = ⟨X', Z'⟩ by rfl] at hIdXZ hind  rw [show YW' = ⟨Y', W'⟩ by rfl] at hIdYW hind  rw [← condRuzsaDist_of_copy hX' hZ' hY' hW' hX hZ hY hW hIdXZ hIdYW,    condRuzsaDist_of_indep hX' hZ' hY' hW' _ hind]  have hIdX : IdentDistrib X X' μ ν := hIdXZ.symm.comp measurable_fst  have hIdY : IdentDistrib Y Y' μ' ν := hIdYW.symm.comp measurable_fst  rw [hIdX.rdist_congr hIdY, hIdXZ.symm.mutualInfo_eq, hIdYW.symm.mutualInfo_eq,    hind'.rdist_eq hX' hY', mutualInfo_eq_entropy_sub_condEntropy hX' hZ',    mutualInfo_eq_entropy_sub_condEntropy hY' hW']  have h := condEntropy_le_entropy ν (X := X' - Y') (hX'.sub hY') (hZ'.prodMk hW')  linarith [h, entropy_nonneg Z' ν, entropy_nonneg W' ν]