condRho_of_sum_le

lemma condRho_of_sum_le [IsProbabilityMeasure μ]    (hX : Measurable X) (hY : Measurable Y) (hA : A.Nonempty) (h_indep : IndepFun X Y μ) :    ρ[X | X + Y ; μ # A] ≤ (ρ[X ; μ # A] + ρ[Y ; μ # A] + d[ X ; μ # Y ; μ ]) / 2 := by  have I : ρ[X | X + Y ; μ # A] ≤ ρ[X ; μ # A] + (H[X ; μ] - H[X | X + Y ; μ]) / 2 :=    condRho_le hX (by fun_prop) hA  have I' : H[X ; μ] - H[X | X + Y ; μ] = H[X + Y ; μ] - H[Y ; μ] := by    rw [ProbabilityTheory.chain_rule'' _ hX (by fun_prop), entropy_add_right hX hY,      IndepFun.entropy_pair_eq_add hX hY h_indep]    abel  have J : ρ[Y | Y + X ; μ # A] ≤ ρ[Y ; μ # A] + (H[Y ; μ] - H[Y | Y + X ; μ]) / 2 :=    condRho_le hY (by fun_prop) hA  have J' : H[Y ; μ] - H[Y | Y + X ; μ] = H[Y + X ; μ] - H[X ; μ] := by    rw [ProbabilityTheory.chain_rule'' _ hY (by fun_prop), entropy_add_right hY hX,      IndepFun.entropy_pair_eq_add hY hX h_indep.symm]    abel  have : Y + X = X + Y := by abel  simp only [this] at J J'  have : ρ[X | X + Y ; μ # A] = ρ[Y | X + Y ; μ # A] := by    simp only [condRho]    congr with s    congr 1    have : ρ[X ; μ[|(X + Y) ⁻¹' {s}] # A] = ρ[fun ω ↦ X ω + s ; μ[|(X + Y) ⁻¹' {s}] # A] := by      rw [rho_of_translate hX hA]    rw [this]    apply rho_eq_of_identDistrib    apply IdentDistrib.of_ae_eq (by fun_prop)    have : MeasurableSet ((X + Y) ⁻¹' {s}) := by      have : Measurable (X + Y) := by fun_prop      exact this (measurableSet_singleton _)    filter_upwards [ae_cond_mem this] with a ha    simp only [mem_preimage, Pi.add_apply, mem_singleton_iff] at ha    rw [← ha]    nth_rewrite 1 [← ZModModule.neg_eq_self (X a)]    abel  have : X - Y = X + Y := ZModModule.sub_eq_add _ _  rw [h_indep.rdist_eq hX hY, sub_eq_add_neg, this]  linarith