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

ProbabilityTheory.mutualInfo_nonneg

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:725 to 736

Source documentation

Mutual information is non-negative.

Exact Lean statement

lemma mutualInfo_nonneg (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω)
    [FiniteRange X] [FiniteRange Y] :
    0 ≤ I[X : Y ; μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma mutualInfo_nonneg (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω)    [FiniteRange X] [FiniteRange Y] :    0 ≤ I[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]  exact measureMutualInfo_nonneg