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

ProbabilityTheory.condEntropy_eq_kernel_entropy

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:383 to 394

Source documentation

Conditional entropy of a random variable is equal to the entropy of its conditional kernel.

Exact Lean statement

lemma condEntropy_eq_kernel_entropy [Nonempty S] [Countable S] [MeasurableSingletonClass S]
    (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) [IsFiniteMeasure μ] [FiniteRange Y] :
    H[X | Y ; μ] = Hk[condDistrib X Y μ, μ.map Y]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condEntropy_eq_kernel_entropy [Nonempty S] [Countable S] [MeasurableSingletonClass S]    (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) [IsFiniteMeasure μ] [FiniteRange Y] :    H[X | Y ; μ] = Hk[condDistrib X Y μ, μ.map Y] := by  rw [condEntropy_def, Kernel.entropy]  apply integral_congr_finiteSupport  intro t ht  rw [Measure.map_apply hY (.singleton _)] at ht  simp only [entropy_def]  congr  ext s hs  rw [condDistrib_apply' hX hY _ _ ht hs, Measure.map_apply hX hs,      cond_apply (hY (.singleton _))]