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

ProbabilityTheory.Kernel.max_entropy_le_entropy_mul_prod

PFR.ForMathlib.Entropy.Kernel.Group · PFR/ForMathlib/Entropy/Kernel/Group.lean:136 to 148

Mathematical statement

Exact Lean statement

@[to_additive]
lemma max_entropy_le_entropy_mul_prod
    (κ : Kernel T G) [IsMarkovKernel κ] (η : Kernel T G) [IsMarkovKernel η]
    (μ : Measure T) [IsZeroOrProbabilityMeasure μ] [FiniteSupport μ]
    (hκ : AEFiniteKernelSupport κ μ) (hη : AEFiniteKernelSupport η μ) :
    max (Hk[κ, μ]) (Hk[η, μ]) ≤ Hk[map (κ ×ₖ η) (fun p ↦ p.1 * p.2), μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[to_additive]lemma max_entropy_le_entropy_mul_prod    (κ : Kernel T G) [IsMarkovKernel κ] (η : Kernel T G) [IsMarkovKernel η]    (μ : Measure T) [IsZeroOrProbabilityMeasure μ] [FiniteSupport μ]    (hκ : AEFiniteKernelSupport κ μ) (hη : AEFiniteKernelSupport η μ) :    max (Hk[κ, μ]) (Hk[η, μ]) ≤ Hk[map (κ ×ₖ η) (fun p ↦ p.1 * p.2), μ] := by  calc max (Hk[κ, μ]) (Hk[η, μ])    = max (Hk[κ, μ]) (Hk[η, μ]) - Ik[κ ×ₖ η, μ] := by        rw [mutualInfo_prod _ hκ hη, sub_zero]  _ ≤ Hk[map (κ ×ₖ η) (fun p ↦ p.1 * p.2), μ] := by        convert max_entropy_sub_mutualInfo_le_entropy_mul (κ ×ₖ η) μ (hκ.prod hη)        · simp        · simp