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

ProbabilityTheory.Kernel.entropy_triple_add_entropy_le

PFR.ForMathlib.Entropy.Kernel.MutualInfo · PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean:390 to 404

Source documentation

The submodularity inequality: $H[X,Y,Z] + H[Z] \leq H[X,Z] + H[Y,Z].$

Exact Lean statement

lemma entropy_triple_add_entropy_le (κ : Kernel T (S × U × V)) [IsZeroOrMarkovKernel κ]
    (μ : Measure T) [IsZeroOrProbabilityMeasure μ] [FiniteSupport μ]
    (hκ : AEFiniteKernelSupport κ μ) :
    Hk[κ, μ] + Hk[snd (snd κ), μ] ≤ Hk[deleteMiddle κ, μ] + Hk[snd κ, μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma entropy_triple_add_entropy_le (κ : Kernel T (S × U × V)) [IsZeroOrMarkovKernel κ]    (μ : Measure T) [IsZeroOrProbabilityMeasure μ] [FiniteSupport μ]    (hκ : AEFiniteKernelSupport κ μ) :    Hk[κ, μ] + Hk[snd (snd κ), μ] ≤ Hk[deleteMiddle κ, μ] + Hk[snd κ, μ] := by  have h2 : fst (reverse κ) = snd (snd κ) := by    rw [fst_eq, reverse_eq, snd_eq, map_map _ (by fun_prop) (by fun_prop), snd_eq,      map_map _ (by fun_prop) (by fun_prop)]    congr  rw [← entropy_reverse hκ, ← h2]  refine (entropy_triple_add_entropy_le' (κ := reverse κ) (μ:= μ) hκ.reverse).trans ?_  refine add_le_add ?_ ?_  · rw [← entropy_swapRight]    simp  · rw [← entropy_swapRight]    simp