condRhoMinus_le

lemma condRhoMinus_le [IsZeroOrProbabilityMeasure μ] {S : Type*} [MeasurableSpace S]    [Finite S] [MeasurableSingletonClass S]    {Z : Ω → S} (hX : Measurable X) (hZ : Measurable Z) (hA : A.Nonempty) :    ρ⁻[X | Z ; μ # A] ≤ ρ⁻[X ; μ # A] + H[X ; μ] - H[X | Z ; μ] := by  cases nonempty_fintype S  have : IsProbabilityMeasure (uniformOn (A : Set G)) := by    apply isProbabilityMeasure_uniformOn A.finite_toSet hA  suffices ρ⁻[X | Z ; μ # A] - H[X ; μ] + H[X | Z ; μ] ≤ ρ⁻[X ; μ # A] by linarith  apply le_csInf (nonempty_rhoMinusSet hA)  rintro - ⟨μ', hμ', habs, rfl⟩  rw [condRhoMinus, tsum_fintype]  let _ : MeasureSpace (G × G) := ⟨μ'.prod (uniformOn (A : Set G))⟩  have hP : (ℙ : Measure (G × G)) = μ'.prod (uniformOn (A : Set G)) := rfl  have : IsProbabilityMeasure (ℙ : Measure (G × G)) := by rw [hP]; infer_instance  have : ∑ b : S, μ.real (Z ⁻¹' {b}) * ρ⁻[X ; μ[|Z ← b] # A]      ≤ KL[ X | Z ; μ # (Prod.fst + Prod.snd : G × G → G) ; ℙ] := by    rw [condKLDiv, tsum_fintype]    apply Finset.sum_le_sum (fun i hi ↦ ?_)    gcongr    apply rhoMinus_le_def hX (fun y hy ↦ ?_)    have T := habs y hy    rw [Measure.map_apply hX (measurableSet_singleton _)] at T ⊢    exact cond_absolutelyContinuous T  rw [condKLDiv_eq hX hZ (by exact habs)] at this  rw [← hP]  linarith