InformationTheory.Shannon.BroadcastChannel.ConverseGateway

Imports 9

Degraded broadcast channel — converse single-letterization #

Chain-rule material for the converse of the degraded broadcast channel (BC) coding theorem (Cover–Thomas). The single-letterization introduces auxiliary variables Uᵢ = (W₂, Y₂^{i-1}) and splits into two bounds:

the R₂-side bound I(W₂; Y₂ⁿ) ≤ ∑ᵢ I(Uᵢ; Y_{2,i}) — chain-rule plumbing on a prefix conditioner.
the R₁-side bound I(W₁; Y₁ⁿ | W₂) = ∑ᵢ I(Xᵢ; Y_{1,i} | Uᵢ) — this one requires the Csiszár sum identity to swap the prefix conditioner Y₁^{i-1} ↔ Y₂^{i-1} under degradedness X → Y₁ → Y₂.

Implementation notes #

The Csiszár sum identity is a rearrangement of the mutual-information chain rule, but it is stated over suffix sequences B_{i+1}ⁿ whereas the rest of the chain-rule API here is prefix-based (Y^{<i}); its proof therefore goes through the reflection-based condMutualInfo_suffix_chain_rule.

theorem

InformationTheory.Shannon.BroadcastChannel.mutualInfo_chain_rule_Y_fin'

source

{Ω : Type u_1} [MeasurableSpace Ω] {m : ℕ} {δ : Type u_2} {γ : Type u_3} [MeasurableSpace δ] [StandardBorelSpace δ] [Nonempty δ] [Fintype γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] [StandardBorelSpace γ] [Nonempty γ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (W : Ω → δ) (Bs : Fin m → Ω → γ) (hW : Measurable W) (hBs : ∀ (i : Fin m), Measurable (Bs i)) :

(mutualInfo μ W fun (ω : Ω) (j : Fin m) => Bs j ω) = ∑ i : Fin m, condMutualInfo μ W (Bs i) fun (ω : Ω) (j : Fin ↑i) => Bs ⟨↑j, ⋯⟩ ω

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.mutualInfo_chain_rule_Y_fin

source

{Ω : Type u_1} [MeasurableSpace Ω] {γ : Type u_2} [Fintype γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] [StandardBorelSpace γ] {n : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (W : Ω → γ) (Bs : Fin n → Ω → γ) (hW : Measurable W) (hBs : ∀ (i : Fin n), Measurable (Bs i)) :

(mutualInfo μ W fun (ω : Ω) (j : Fin n) => Bs j ω) = ∑ i : Fin n, condMutualInfo μ W (Bs i) fun (ω : Ω) (j : Fin ↑i) => Bs ⟨↑j, ⋯⟩ ω

Chain rule for mutual information expanded along the sequence argument: I(W; Bⁿ) = ∑ᵢ I(W; Bᵢ | B^{<i}).

Derived from the left-axis mutualInfo_chain_rule_fin by mutualInfo_comm + condMutualInfo_comm. The conditioner is the prefix B^{<i} only. @audit:ok

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.bc_converse_bound_a

source

{Ω : Type u_1} [MeasurableSpace Ω] {γ : Type u_2} [Fintype γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] [StandardBorelSpace γ] {n : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (W₂ : Ω → γ) (Y₂s : Fin n → Ω → γ) (hW₂ : Measurable W₂) (hY₂s : ∀ (i : Fin n), Measurable (Y₂s i)) :

(mutualInfo μ W₂ fun (ω : Ω) (j : Fin n) => Y₂s j ω).toReal ≤ ∑ i : Fin n, (mutualInfo μ (fun (ω : Ω) => (W₂ ω, fun (j : Fin ↑i) => Y₂s ⟨↑j, ⋯⟩ ω)) (Y₂s i)).toReal

Receiver-2 single-letterization for the BC converse: with Uᵢ = (W₂, Y₂^{i-1}), the message–output mutual information obeys I(W₂; Y₂ⁿ) ≤ ∑ᵢ I(Uᵢ; Y_{2,i}).

Chain-rule plumbing: expand I(W₂; Y₂ⁿ) along the sequence argument into ∑ᵢ I(W₂; Y_{2,i} | Y₂^{i-1}), then bound each summand by I((W₂, Y₂^{i-1}); Y_{2,i}) (adding the prefix to the data variable can only increase mutual information). @audit:ok

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.csiszar_sum_identity

source

{Ω : Type u_1} [MeasurableSpace Ω] {γ : Type u_2} [Fintype γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] [StandardBorelSpace γ] {n : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (As 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, ⋯⟩ ω

Csiszár sum identity (the key ingredient of the R₁-side bound): for any two finite-alphabet sequences As, Bs over Fin n, ∑ᵢ 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ⱼ. Both sides expand (via the prefix chain rule condMutualInfo_prefix_chain_rule for the left, the reflection-based suffix chain rule condMutualInfo_suffix_chain_rule for 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 (El Gamal–Kim). @audit:ok

Used by