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

ProbabilityTheory.cond_chain_rule'

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:618 to 632

Source documentation

If X : Ω → S, Y : Ω → T, Z : Ω → U are random variables, then H[X, Y | Z] = H[X | Z] + H[Y|X, Z].

Exact Lean statement

lemma cond_chain_rule' (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :
    H[⟨X, Y⟩ | Z ; μ] = H[X | Z ; μ] + H[Y | ⟨X, Z⟩ ; μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma cond_chain_rule' (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)    [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :    H[⟨X, Y⟩ | Z ; μ] = H[X | Z ; μ] + H[Y | ⟨X, Z⟩ ; μ] := by  rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ  · simp  have : Nonempty S := Nonempty.map X (μ.nonempty_of_neZero)  have : Nonempty T := Nonempty.map Y (μ.nonempty_of_neZero)  rw [condEntropy_eq_kernel_entropy (hX.prodMk hY) hZ, Kernel.chain_rule]  · congr 1    · rw [condEntropy_eq_kernel_entropy hX hZ]      refine Kernel.entropy_congr ?_      exact condDistrib_fst_ae_eq hX hY hZ μ    · rw [condEntropy_two_eq_kernel_entropy hY hX hZ]  exact Kernel.aefiniteKernelSupport_condDistrib _ _ μ (by measurability) (by measurability)