InformationTheory.Shannon.CondMIChainRule

Imports 5

Conditional mutual-information chain rule over a `Fin`-prefix #

The n-variable conditional chain rule for mutual information with a background conditioner Z carried throughout:

I(A^{<m}; C | Z) = ∑_{k < m} I(A_k; C | (Z, A^{<k})).

This is the conditional analogue of mutualInfo_chain_rule_fin, obtained by an additive induction (mutualInfo_prefix_chain_rule_add) followed by cancellation of the common term I(Z; C). The additive formulation has a clean base case (the empty prefix reshapes (Z, ⟨⟩) ≃ᵐ Z), avoiding any constant-random-variable measure computation.

Main statements #

mutualInfo_prefix_chain_rule_add — I((Z, A^{<m}); C) = I(Z; C) + ∑_{k<m} I(A_k; C | (Z, A^{<k})).
condMutualInfo_prefix_chain_rule — I(A^{<m}; C | Z) = ∑_{k<m} I(A_k; C | (Z, A^{<k})).

def

InformationTheory.Shannon.piReindexMeasurableEquiv

source

{γ : Type u_2} [MeasurableSpace γ] {ι : Type u_5} {ι' : Type u_6} (σ : ι ≃ ι') :

(ι → γ) ≃ᵐ (ι' → γ)

Reindex a (constant-family) function space by an index Equiv, as a MeasurableEquiv. Both directions are coordinatewise evaluations, hence measurable; no StandardBorelSpace needed. Avoids the dependent casts of MeasurableEquiv.piCongrLeft.

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

InformationTheory.Shannon.revSuffixEquiv

source

{n : ℕ} (i : Fin n) :

{ j : Fin n // ↑i < ↑j } ≃ Fin (n - 1 - ↑i)

The order-reversing reindex of the strict-upper-set {j : Fin n // i < j} onto Fin (n - 1 - i), sending j ↦ n - 1 - j (so the largest index maps to 0).

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

theorem

InformationTheory.Shannon.mutualInfo_prefix_chain_rule_add

source

{Ω : Type u_1} [MeasurableSpace Ω] {γ : Type u_2} [MeasurableSpace γ] [StandardBorelSpace γ] [Nonempty γ] {δ : Type u_3} [MeasurableSpace δ] [StandardBorelSpace δ] [Nonempty δ] {ζ : Type u_4} [MeasurableSpace ζ] {m : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (As : Fin m → Ω → γ) (C : Ω → δ) (Z : Ω → ζ) (hAs : ∀ (i : Fin m), Measurable (As i)) (hC : Measurable C) (hZ : Measurable Z) :

mutualInfo μ (fun (ω : Ω) => (Z ω, fun (j : Fin m) => As j ω)) C = mutualInfo μ Z C + ∑ k : Fin m, condMutualInfo μ (As k) C fun (ω : Ω) => (Z ω, fun (j : Fin ↑k) => As ⟨↑j, ⋯⟩ ω)

Additive prefix chain rule: prepending a Fin m prefix of As to the background conditioner Z decomposes the mutual information additively as I((Z, A^{<m}); C) = I(Z; C) + ∑_{k<m} I(A_k; C | (Z, A^{<k})). Proven by induction on m. @audit:ok

Used by

theorem

InformationTheory.Shannon.condMutualInfo_prefix_chain_rule

source

condMutualInfo μ (fun (ω : Ω) (j : Fin m) => As j ω) C Z = ∑ k : Fin m, condMutualInfo μ (As k) C fun (ω : Ω) => (Z ω, fun (j : Fin ↑k) => As ⟨↑j, ⋯⟩ ω)

Conditional prefix chain rule: I(A^{<m}; C | Z) = ∑_{k<m} I(A_k; C | (Z, A^{<k})).

Derived from the additive form by cancelling the common term I(Z; C) (requires it finite). @audit:ok

Used by

theorem

InformationTheory.Shannon.condMutualInfo_suffix_chain_rule

source

{Ω : Type u_1} [MeasurableSpace Ω] {γ : Type u_2} [MeasurableSpace γ] [StandardBorelSpace γ] [Nonempty γ] {δ : Type u_3} [MeasurableSpace δ] [StandardBorelSpace δ] [Nonempty δ] {ζ : Type u_4} [MeasurableSpace ζ] {n : ℕ} (i : Fin n) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Bs : Fin n → Ω → γ) (C : Ω → δ) (Z : Ω → ζ) (hBs : ∀ (j : Fin n), Measurable (Bs j)) (hC : Measurable C) (hZ : Measurable Z) (hZC : mutualInfo μ Z C ≠ ⊤) :

condMutualInfo μ (fun (ω : Ω) (j : { j : Fin n // ↑i < ↑j }) => Bs (↑j) ω) C Z = ∑ j : { j : Fin n // ↑i < ↑j }, condMutualInfo μ (Bs ↑j) C fun (ω : Ω) => (Z ω, fun (j' : { j' : Fin n // ↑↑j < ↑j' }) => Bs (↑j') ω)

Conditional suffix chain rule (reflection of the prefix one): I(B^{>i}; C | Z) = ∑_{j > i} I(B_j; C | (Z, B^{>j})), where the left variable expands a suffix B^{>i} = (B_{i+1}, …, B_{n-1}) peeling off each B_j while conditioning on the larger-index suffix B^{>j}. Obtained by reindexing the suffix onto a Fin-prefix with the order-reversing revSuffixEquiv and invoking condMutualInfo_prefix_chain_rule. @audit:ok

Used by

InformationTheory.Shannon.CondMIChainRule

Conditional mutual-information chain rule over a Fin-prefix #

Main statements #

Conditional mutual-information chain rule over a `Fin`-prefix #