ProbabilityTheory.measureMutualInfo_swap

lemma measureMutualInfo_swap (μ : Measure (S × T)) :    Im[μ.map Prod.swap] = Im[μ] := by  rw [measureMutualInfo_def, add_comm, Measure.map_map measurable_snd measurable_swap,    Measure.map_map measurable_fst measurable_swap]  congr 1  simp_rw [measureEntropy, Measure.map_apply measurable_swap MeasurableSet.univ]  simp only [Set.preimage_univ, Measure.ennreal_smul_real_apply, smul_eq_mul]  simp_rw [map_measureReal_apply measurable_swap (.singleton _)]  have : Set.range (Prod.swap : S × T → T × S) = .univ := Set.range_eq_univ.mpr Prod.swap_surjective  rw [← tsum_univ, ← this,    tsum_range (fun x ↦ negMulLog <| (μ Set.univ)⁻¹.toReal * μ.real (Prod.swap⁻¹' {x}))      Prod.swap_injective]  congr! with ⟨s, t⟩  simpa using Prod.swap_injective.preimage_image {(s, t)}