ProbabilityTheory.mutualInfo_eq_zero

lemma mutualInfo_eq_zero (hX : Measurable X) (hY : Measurable Y) {μ : Measure Ω}    [IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] :    I[X : Y ; μ] = 0 ↔ IndepFun X Y μ := by  simp_rw [mutualInfo_def, entropy_def]  have h_fst : μ.map X = (μ.map (⟨X, Y⟩)).map Prod.fst := by    rw [Measure.map_map measurable_fst (hX.prodMk hY)]    congr  have h_snd : μ.map Y = (μ.map (⟨X, Y⟩)).map Prod.snd := by    rw [Measure.map_map measurable_snd (hX.prodMk hY)]    congr  rw [h_fst, h_snd, ← measureMutualInfo.eq_def, measureMutualInfo_eq_zero_iff]  simp [indepFun_iff_map_prod_eq_prod_map_map hX.aemeasurable hY.aemeasurable,    Measure.ext_iff_measureReal_singleton_finiteSupport,    Measure.map_map measurable_fst (hX.prodMk hY),    Measure.map_map measurable_snd (hX.prodMk hY), ← measureReal_prod_prod, Function.comp_def]