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

ProbabilityTheory.Kernel.entropy_prod

PFR.ForMathlib.Entropy.Kernel.Basic · PFR/ForMathlib/Entropy/Kernel/Basic.lean:377 to 386

Mathematical statement

Exact Lean statement

@[simp]
lemma entropy_prod {κ : Kernel T S} {η : Kernel T U} [IsMarkovKernel κ] [IsMarkovKernel η]
    {μ : Measure T} [IsZeroOrProbabilityMeasure μ] [FiniteSupport μ]
    (hκ : AEFiniteKernelSupport κ μ) (hη : AEFiniteKernelSupport η μ) :
    Hk[κ ×ₖ η, μ] = Hk[κ, μ] + Hk[η, μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[simp]lemma entropy_prod {κ : Kernel T S} {η : Kernel T U} [IsMarkovKernel κ] [IsMarkovKernel η]    {μ : Measure T} [IsZeroOrProbabilityMeasure μ] [FiniteSupport μ]    (hκ : AEFiniteKernelSupport κ μ) (hη : AEFiniteKernelSupport η μ) :    Hk[κ ×ₖ η, μ] = Hk[κ, μ] + Hk[η, μ] := by  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ  · simp  have : Nonempty U := nonempty_of_isProbabilityMeasure_of_isMarkovKernel μ η  rw [chain_rule (hκ.prod hη), fst_prod,    entropy_congr (condKernel_prod_ae_eq _ _), entropy_prodMkRight hκ]