condKLDiv_eq

lemma condKLDiv_eq {S : Type*} [MeasurableSpace S] [Finite S] [MeasurableSingletonClass S]    [Finite G] [IsZeroOrProbabilityMeasure μ] [IsFiniteMeasure μ']    {X : Ω → G} {Y : Ω' → G} {Z : Ω → S}    (hX : Measurable X) (hZ : Measurable Z)    (habs : ∀ x, μ'.map Y {x} = 0 → μ.map X {x} = 0) :    KL[ X | Z ; μ # Y ; μ'] = KL[X ; μ # Y ; μ'] + H[X ; μ] - H[ X | Z ; μ] := by  cases nonempty_fintype G  cases nonempty_fintype S  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ  · simp [condKLDiv, tsum_fintype, KLDiv_eq_sum, Finset.mul_sum, entropy_eq_sum]  simp only [condKLDiv, tsum_fintype, KLDiv_eq_sum, Finset.mul_sum, entropy_eq_sum]  rw [Finset.sum_comm, condEntropy_eq_sum_sum_fintype hZ, Finset.sum_comm (α := G),    ← Finset.sum_add_distrib, ← Finset.sum_sub_distrib]  congr with g  simp only [negMulLog, neg_mul, Finset.sum_neg_distrib, mul_neg, sub_neg_eq_add, ← sub_eq_add_neg,    ← mul_sub]  simp_rw [← map_measureReal_apply hZ (measurableSet_singleton _)]  have A : Measure.map X μ {g} = ∑ x, μ.map Z {x} * (Measure.map X μ[|Z ⁻¹' {x}] {g}) := by    simp_rw [Measure.map_apply hZ (measurableSet_singleton _)]    have : Measure.map X μ {g} = Measure.map X (∑ x, μ (Z ⁻¹' {x}) • μ[|Z ⁻¹' {x}]) {g} := by      rw [sum_meas_smul_cond_fiber hZ μ]    rw [← MeasureTheory.Measure.sum_fintype, Measure.map_sum hX.aemeasurable] at this    simpa using this  have : (Measure.map X μ).real {g} =      ∑ x, (Measure.map Z μ).real {x} * (Measure.map X μ[|Z ⁻¹' {x}]).real {g} := by    rw [measureReal_def, A, ENNReal.toReal_sum (fun a ha ↦ by finiteness)]    congr with x    rw [ENNReal.toReal_mul]    rfl  nth_rewrite 1 [this]  rw [Finset.sum_mul, ← Finset.sum_add_distrib]  congr with s  rw [mul_assoc, ← mul_add, ← mul_add]  rcases eq_or_ne ((Measure.map Z μ).real {s}) 0 with hs | hs  · simp [hs]  rcases eq_or_ne ((Measure.map X μ[|Z ⁻¹' {s}]).real {g}) 0 with hg | hg  · simp [hg]  congr  have hXg : (μ.map X).real {g} ≠ 0 := by    intro h    rw [this, Finset.sum_eq_zero_iff_of_nonneg (fun a ha ↦ by positivity)] at h    specialize h s (Finset.mem_univ _)    rw [mul_eq_zero] at h    tauto  have hYg : μ'.map Y {g} ≠ 0 := fun h ↦ by simp [measureReal_def, habs _ h] at hXg  have hYg' : (μ'.map Y).real {g} ≠ 0 := by simp [measureReal_eq_zero_iff, hYg]  rw [Real.log_div hg hYg', Real.log_div hXg hYg']  abel