rhoMinus_of_sum

lemma rhoMinus_of_sum [IsZeroOrProbabilityMeasure μ]    (hX : Measurable X) (hY : Measurable Y)    (hA : A.Nonempty) (h_indep : IndepFun X Y μ) :    ρ⁻[X + Y ; μ # A] ≤ ρ⁻[X ; μ # A] := by  rcases eq_zero_or_isProbabilityMeasure μ with hμ | hμ  · simp [rhoMinus_zero_measure hμ]  apply le_csInf (nonempty_rhoMinusSet hA)  have : IsProbabilityMeasure (uniformOn (A : Set G)) :=    isProbabilityMeasure_uniformOn A.finite_toSet hA  rintro - ⟨μ', μ'_prob, habs, rfl⟩  obtain ⟨Ω', hΩ', m, X', Y', T, U, hm, h_indep', hX', hY', hT, hU, hXX', hYY', hTμ, hU_unif⟩ :=    independent_copies4_nondep (X₁ := X) (X₂ := Y) (X₃ := id) (X₄ := id) hX hY measurable_id    measurable_id μ μ μ' (uniformOn (A : Set G))  let _ : MeasureSpace Ω' := ⟨m⟩  have hP : (ℙ : Measure Ω') = m := rfl  have hTU : IdentDistrib (T + U) (Prod.fst + Prod.snd) ℙ (μ'.prod (uniformOn (A : Set G))) := by    apply IdentDistrib.add    · exact hTμ.trans IdentDistrib.fst_id.symm    · exact hU_unif.trans IdentDistrib.snd_id.symm    · exact h_indep'.indepFun (i := 2) (j := 3) (by simp)    · exact indepFun_fst_snd  have hXY : IdentDistrib (X + Y) (X' + Y') μ ℙ := by    apply IdentDistrib.add hXX'.symm hYY'.symm h_indep    exact h_indep'.indepFun zero_ne_one  have hX'TUY' : IndepFun (⟨X', T + U⟩) Y' ℙ := by    have I : iIndepFun ![X', Y', T + U] m :=      ProbabilityTheory.iIndepFun.apply_two_last h_indep' hX' hY' hT hU        (phi := fun a b ↦ a + b) (by fun_prop)    exact (I.reindex_three_bac.pair_last_of_three hY' hX' (by fun_prop)).symm  have I₁ : ρ⁻[X + Y ; μ # A] ≤ KL[X + Y ; μ # (T + Y') + U ; ℙ] := by    apply rhoMinus_le (by fun_prop) hA _ (by fun_prop) (by fun_prop)    · have : iIndepFun ![U, X', T, Y'] := h_indep'.reindex_four_dacb      have : iIndepFun ![U, X', T + Y'] :=        this.apply_two_last (phi := fun a b ↦ a + b) hU hX' hT hY' (by fun_prop)      apply this.indepFun (i := 2) (j := 0)      simp    · rw [hXY.map_eq]      have : T + Y' + U = (T + U) + Y' := by abel      rw [this]      apply absolutelyContinuous_add_of_indep hX'TUY' hX' (by fun_prop) hY'      rw [hTU.map_eq, hP, hXX'.map_eq]      exact habs    · exact isUniform_uniformOn.of_identDistrib hU_unif.symm A.measurableSet  have I₂ : KL[X + Y ; μ # (T + Y') + U ; ℙ] = KL[X' + Y' # (T + U) + Y'] := by    apply IdentDistrib.KLDiv_eq _ _ hXY    have : T + Y' + U = T + U + Y' := by abel    rw [this]    exact .refl <| by fun_prop  have I₃ : KL[X' + Y' # (T + U) + Y'] ≤ KL[X' # T + U] := by    apply KLDiv_add_le_KLDiv_of_indep _ (by fun_prop) (by fun_prop) (by fun_prop)    · rw [hTU.map_eq, hP, hXX'.map_eq]      exact habs    · exact hX'TUY'  have I₄ : KL[X' # T + U] = KL[X ; μ # Prod.fst + Prod.snd ; μ'.prod (uniformOn (A : Set G))] :=    IdentDistrib.KLDiv_eq _ _ hXX' hTU  exact ((I₁.trans_eq I₂).trans I₃).trans_eq I₄