Source indexedlemma · leanprover/lean4:v4.33.0-rc1

ProbabilityTheory.measureMutualInfo_univ_smul

PFR.ForMathlib.Entropy.Measure · PFR/ForMathlib/Entropy/Measure.lean:538 to 553

Mathematical statement

Exact Lean statement

lemma measureMutualInfo_univ_smul (μ : Measure (S × U)) : Im[(μ Set.univ)⁻¹ • μ] = Im[μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma measureMutualInfo_univ_smul (μ : Measure (S × U)) : Im[(μ Set.univ)⁻¹ • μ] = Im[μ] := by  by_cases hμ_fin : IsFiniteMeasure μ  swap  · rw [measureMutualInfo_of_not_isFiniteMeasure hμ_fin]    rw [not_isFiniteMeasure_iff] at hμ_fin    simp [hμ_fin]  rcases eq_zero_or_neZero μ with hμ | _  · simp [hμ]  rw [measureMutualInfo_def, measureMutualInfo_def]  congr 1  · congr 1    · convert measureEntropy_univ_smul      simp [Measure.map_smul, Measure.map_apply measurable_fst]    · convert measureEntropy_univ_smul      simp [Measure.map_smul, Measure.map_apply measurable_snd]  convert measureEntropy_univ_smul