ProbabilityTheory.measureMutualInfo_of_not_isFiniteMeasure

lemma measureMutualInfo_of_not_isFiniteMeasure {μ : Measure (S × U)} (h : ¬ IsFiniteMeasure μ) :    Im[μ] = 0 := by  rw [measureMutualInfo_def]  have h1 : ¬ IsFiniteMeasure (μ.map Prod.fst) := by    rw [not_isFiniteMeasure_iff] at h ⊢    rw [← h]    exact Measure.map_apply measurable_fst MeasurableSet.univ  have h2 : ¬ IsFiniteMeasure (μ.map Prod.snd) := by    rw [not_isFiniteMeasure_iff] at h ⊢    rw [← h]    exact Measure.map_apply measurable_snd MeasurableSet.univ  rw [measureEntropy_of_not_isFiniteMeasure h, measureEntropy_of_not_isFiniteMeasure h1,    measureEntropy_of_not_isFiniteMeasure h2]  simp