KLDiv_eq_zero_iff_identDistrib

lemma KLDiv_eq_zero_iff_identDistrib [Finite G] [MeasurableSingletonClass G]    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] (hX : Measurable X) (hY : Measurable Y)    (habs : ∀ x, (μ'.map Y).real {x} = 0 → (μ.map X).real {x} = 0) :    KL[X ; μ # Y ; μ'] = 0 ↔ IdentDistrib X Y μ μ' := by  cases nonempty_fintype G  refine ⟨fun h ↦ ?_, fun h ↦ by simp [KLDiv, h.map_eq]⟩  let νY := μ'.map Y  have : IsProbabilityMeasure νY := Measure.isProbabilityMeasure_map hY.aemeasurable  let νX := μ.map X  have : IsProbabilityMeasure νX := Measure.isProbabilityMeasure_map hX.aemeasurable  obtain ⟨r, hr⟩ : ∃ (r : ℝ), ∀ x ∈ Finset.univ, (νX.real {x}) = r * νY.real {x} := by    apply sum_mul_log_div_eq_iff (by simp) (by simp) fun i _ hi ↦ ?_    · simpa [KLDiv_eq_sum] using h    · simp [habs i hi, νX]  have r_eq : r = 1 := by    have : r * ∑ x, νY.real {x} = ∑ x, νX.real {x} := by      simp only [Finset.mul_sum, Finset.mem_univ, hr]    simpa using this  have : νX = νY := by    apply Measure.ext_iff_singleton.mpr (fun x ↦ ?_)    simpa [Measure.real, r_eq, ENNReal.toReal_eq_toReal_iff'] using hr x (Finset.mem_univ _)  exact ⟨hX.aemeasurable, hY.aemeasurable, this⟩