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

ProbabilityTheory.condMutualInfo_eq

PFR.ForMathlib.Entropy.Basic · PFR/ForMathlib/Entropy/Basic.lean:938 to 950

Source documentation

I[X : Y| Z] = H[X| Z] + H[Y| Z] - H[X, Y| Z].

Exact Lean statement

lemma condMutualInfo_eq [Countable U]
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ] [FiniteRange Z] :
    I[X : Y | Z ; μ] = H[X | Z ; μ] + H[Y | Z; μ] - H[⟨X, Y⟩ | Z ; μ]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma condMutualInfo_eq [Countable U]    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)    (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ] [FiniteRange Z] :    I[X : Y | Z ; μ] = H[X | Z ; μ] + H[Y | Z; μ] - H[⟨X, Y⟩ | 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 [condMutualInfo_eq_kernel_mutualInfo hX hY hZ, Kernel.mutualInfo,    Kernel.entropy_congr (condDistrib_fst_ae_eq hX hY hZ _),    Kernel.entropy_congr (condDistrib_snd_ae_eq hX hY hZ _),    condEntropy_eq_kernel_entropy hX hZ, condEntropy_eq_kernel_entropy hY hZ,    condEntropy_eq_kernel_entropy (hX.prodMk hY) hZ]