rhoMinus_le

lemma rhoMinus_le [IsZeroOrProbabilityMeasure μ]    (hX : Measurable X) (hA : A.Nonempty)    {Ω' : Type*} [MeasurableSpace Ω'] {T : Ω' → G} {U : Ω' → G} {μ' : Measure Ω'}    [IsProbabilityMeasure μ'] (hunif : IsUniform A U μ') (hT : Measurable T)    (hU : Measurable U) (h_indep : IndepFun T U μ')    (habs : ∀ y, (μ'.map (T + U)) {y} = 0 → μ.map X {y} = 0) :    ρ⁻[X ; μ # A] ≤ KL[X ; μ # T + U ; μ'] := by  cases nonempty_fintype G  have : IsProbabilityMeasure (μ'.map T) := isProbabilityMeasure_map hT.aemeasurable  have : IsProbabilityMeasure (uniformOn (A : Set G)) :=    isProbabilityMeasure_uniformOn A.finite_toSet hA  have E : μ'.map U = uniformOn (A : Set G) := hunif.map_eq_uniformOn hU A.finite_toSet hA  have M : (Measure.map (Prod.fst + Prod.snd) ((μ'.map T).prod (uniformOn ↑A))) =      (Measure.map (T + U) μ') := by    ext s _    rw [h_indep.map_add_eq_sum hT hU]    have : IndepFun Prod.fst Prod.snd ((μ'.map T).prod (uniformOn (A : Set G))) :=      ProbabilityTheory.indepFun_fst_snd    rw [this.map_add_eq_sum measurable_fst measurable_snd,      Measure.map_fst_prod, Measure.map_snd_prod]    simp [E]  apply csInf_le (bddBelow_rhoMinusSet hX)  simp only [rhoMinusSet, Set.mem_setOf_eq]  exact ⟨μ'.map T, isProbabilityMeasure_map hT.aemeasurable, by rwa [M], by simp [KLDiv, M]⟩