LeanPool.ZhangYeungInequality.Prelude

Imported Lean Pool material for LeanPool.ZhangYeungInequality.Prelude.

Generic Shannon helpers

theorem ZhangYeung.IdentDistrib.condMutualInfo_eq {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {S : Type u_3} {T : Type u_4} {U : Type u_5} [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [MeasurableSingletonClass U] [Finite S] [Finite T] [Finite U] {μ : MeasureTheory.Measure Ω} {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} {X' : Ω' → S} {Y' : Ω' → T} {Z' : Ω' → U} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (hX' : Measurable X') (hY' : Measurable Y') (hZ' : Measurable Z') (h : ProbabilityTheory.IdentDistrib (fun (ω : Ω) => (X ω, Y ω, Z ω)) (fun (ω' : Ω') => (X' ω', Y' ω', Z' ω')) μ μ') : I[X : Y|Z;μ] = I[X' : Y'|Z';μ']

Substituting variables for identically-distributed ones leaves the conditional mutual information unchanged. PFR exposes IdentDistrib.condEntropy_eq and IdentDistrib.mutualInfo_eq but not this conditional-mutual-information transport. The three sub-IdentDistribs for ⟨X, Z⟩, ⟨Y, Z⟩, and ⟨⟨X, Y⟩, Z⟩ are extracted from the triple by one IdentDistrib.comp with a measurable projection each. Promoted from ZhangYeung/CopyLemma.lean as of M5.

theorem ZhangYeung.mutualInfo_add_three_way_identity {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Finite α] [Finite β] [Finite γ] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [MeasurableSingletonClass γ] {X : Ω → α} {Y : Ω → β} {Z : Ω → γ} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : I[X : Y; μ] + I[X : Z; μ] = I[X : prod Y Z; μ] + I[Y : Z; μ] - I[Y : Z|X;μ]

The three-way interaction identity

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

Equivalent to a pair of chain-rule applications on I[X : ⟨Y, Z⟩], together with the defining identity I[Y : Z | X] = I[Y : Z] - I[X : Y : Z] for the three-way interaction information. Promoted from ZhangYeung/Theorem3.lean as of M5.

theorem ZhangYeung.mutualInfo_le_of_condIndepFun {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Finite α] [Finite β] [Finite γ] [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [MeasurableSingletonClass γ] {X : Ω → α} {Y : Ω → β} {Z : Ω → γ} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (h : ProbabilityTheory.CondIndepFun X Y Z μ) : I[X : Y; μ] ≤ I[X : Z; μ]

Data processing for PFR's random-variable form of CondIndepFun: if X and Y are conditionally independent given Z, then I[X : Y] ≤ I[X : Z]. Promoted from ZhangYeung/Theorem3.lean as of M5.

theorem ZhangYeung.condIndepFun_comp {Ω : Type u_1} {α : Type u_2} {α' : Type u_3} {β : Type u_4} {β' : Type u_5} {γ : Type u_6} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace α'] [MeasurableSpace β] [MeasurableSpace β'] [MeasurableSpace γ] {μ : MeasureTheory.Measure Ω} {f : Ω → α} {g : Ω → β} {k : Ω → γ} {φ : α → α'} {ψ : β → β'} (hφ : Measurable φ) (hψ : Measurable ψ) (h : ProbabilityTheory.CondIndepFun f g k μ) : ProbabilityTheory.CondIndepFun (φ ∘ f) (ψ ∘ g) k μ

Post-composition of a CondIndepFun statement on its two measured coordinates by independent measurable functions φ and ψ. The conditioner k is unchanged. Mathlib's CondIndepFun.comp uses the σ-algebra form of conditional independence and does not apply to PFR's random-variable form; this lemma fills that gap by unfolding through condIndepFun_iff to a fibrewise ∀ᵐ-family of IndepFun statements, applying Mathlib's IndepFun.comp inside each fibre, and repackaging. Promoted from ZhangYeung/CopyLemma.lean as of M3 (the second consumer).