rdist_le_avg_ent

lemma rdist_le_avg_ent {X : Ω → G} {Y : Ω' → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X)    (hY : Measurable Y) (μ : Measure Ω := by volume_tac) (μ' : Measure Ω' := by volume_tac)    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] :    d[X ; μ # Y ; μ'] ≤ (H[X ; μ] + H[Y ; μ'])/2 := by  rcases ProbabilityTheory.independent_copies_finiteRange hX hY μ μ'    with ⟨ν, X', Y', hprob, hX', hY', h_indep, hidentX, hidentY, hfinX, hfinY⟩  rw [← hidentX.rdist_congr hidentY,    ← hidentX.entropy_congr, ← IdentDistrib.entropy_congr hidentY,    h_indep.rdist_eq hX' hY']  suffices H[X' - Y'; ν] ≤ H[X'; ν] + H[Y'; ν] by linarith  change H[(fun x ↦ x.1 - x.2) ∘ ⟨X',Y' ⟩; ν] ≤ H[X'; ν] + H[Y'; ν]  exact ((entropy_comp_le ν (by fun_prop) _).trans) (entropy_pair_le_add hX' hY' ν)