InformationTheory

InformationTheory.Shannon.WynerZiv.ConverseGateway

source

Imports 5

Wyner–Ziv converse — heterogeneous Csiszár sum identity (gateway probe) #

This is a gateway-atom probe for the Wyner–Ziv operational converse. It generalizes the same-alphabet csiszar_sum_identity (InformationTheory/Shannon/BroadcastChannel/ConverseGateway.lean) to two sequences over distinct finite alphabets α (the source X) and β (the side information Y).

The Wyner–Ziv converse single-letterization needs the Csiszár sum identity to swap the prefix conditioner X^{i-1} ↔ suffix conditioner Y_{i+1}ⁿ. Because the source and side information live in different alphabets, the same-alphabet identity cannot be reused as-is.

The proof is a direct port of the same-alphabet version: the underlying prefix / suffix conditional chain rules (condMutualInfo_prefix_chain_rule, condMutualInfo_suffix_chain_rule) and the swaps (condMutualInfo_comm, condMutualInfo_map_cond_measurableEquiv) are already polymorphic in the three role types, so the index plumbing is unchanged; only the two sequence alphabets differ.

theorem

InformationTheory.Shannon.WynerZiv.csiszar_sum_identity_hetero

source
{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [Nonempty α] {β : Type u_3} [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] [Nonempty β] {n : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (As : Fin n → Ω → α) (Bs : Fin n → Ω → β) (hAs : ∀ (i : Fin n), Measurable (As i)) (hBs : ∀ (i : Fin n), Measurable (Bs i)) :
(∑ i : Fin n, condMutualInfo μ (fun (ω : Ω) (j : Fin ↑i) => As ⟨↑j, ⋯⟩ ω) (Bs i) fun (ω : Ω) (j : { j : Fin n // ↑i < ↑j }) => Bs (↑j) ω) = ∑ i : Fin n, condMutualInfo μ (fun (ω : Ω) (j : { j : Fin n // ↑i < ↑j }) => Bs (↑j) ω) (As i) fun (ω : Ω) (j : Fin ↑i) => As ⟨↑j, ⋯⟩ ω

Heterogeneous Csiszár sum identity (gateway atom for the Wyner–Ziv converse): for two finite-alphabet sequences As : Fin n → Ω → α and Bs : Fin n → Ω → β over distinct alphabets, ∑ᵢ I(A^{i-1}; Bᵢ | B_{i+1}ⁿ) = ∑ᵢ I(B_{i+1}ⁿ; Aᵢ | A^{i-1}).

Here A^{i-1} is the prefix fun j : Fin i.val ↦ Aⱼ and B_{i+1}ⁿ is the suffix fun j : {j : Fin n // i.val < j.val} ↦ Bⱼ, exactly as in the same-alphabet csiszar_sum_identity. Both sides expand (prefix chain rule on the left, reflection-based suffix chain rule on the right) to the common triangular double sum ∑_{k<i} I(Aₖ; Bᵢ | A^{k-1}, B_{i+1}ⁿ), matched termwise by condMutualInfo_comm plus a prodComm relabel of the conditioner. The distinct alphabets flow through untouched because the chain rules are polymorphic in the sequence / data / conditioner role types. @audit:ok

Used by