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

ProbabilityTheory.Kernel.mutualInfo_nonneg'

PFR.ForMathlib.Entropy.Kernel.MutualInfo · PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean:123 to 131

Mathematical statement

Exact Lean statement

lemma mutualInfo_nonneg' {κ : Kernel T (S × U)} {μ : Measure T} [IsFiniteMeasure μ]
    [FiniteSupport μ] (hκ : FiniteKernelSupport κ) :
    0 ≤ Ik[κ, μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma mutualInfo_nonneg' {κ : Kernel T (S × U)} {μ : Measure T} [IsFiniteMeasure μ]    [FiniteSupport μ] (hκ : FiniteKernelSupport κ) :    0 ≤ Ik[κ, μ] := by  simp_rw [mutualInfo, entropy, integral_eq_setIntegral (ae_mem_support μ),    setIntegral_finset _ .finset, smul_eq_mul]  rw [← Finset.sum_add_distrib, ← Finset.sum_sub_distrib]  simp_rw [← mul_add, ← mul_sub, fst_apply, snd_apply]  have (x : T) : FiniteSupport (κ x) := ⟨hκ x⟩  exact Finset.sum_nonneg fun x _ ↦ mul_nonneg ENNReal.toReal_nonneg measureMutualInfo_nonneg