InformationTheory

InformationTheory.Shannon.BroadcastChannel.OuterBoundUV.Gateway

source

Imports 6

General broadcast channel — chain-rule gateway for the UV outer bound #

Chain-rule material for the Nair–El Gamal (UV) outer bound of the general two-receiver broadcast channel (El Gamal–Kim). The auxiliary variables of that bound mix a prefix of one output sequence with a suffix of the other, Uᵢ = (W₂, Y₁^{<i}, Y₂^{>i}) and Vᵢ = (W₁, Y₁^{<i}, Y₂^{>i}), which needs three pieces of plumbing that the degraded converse (BroadcastChannel.Converse) did not:

  • the reverse-order expansions I(W; Bⁿ) = ∑ᵢ I(W; Bᵢ | B^{>i}) and its conditional form, obtained from the forward expansion by reversing the index;
  • the step I(A; C | Z) ≤ I(B; C | Z) + I(A; C | (Z, B)) that inserts the output suffix into the conditioner;
  • the Csiszár sum identity for two sequences over distinct alphabets carrying a background conditioner, which swaps the prefix conditioner A^{<i} for the suffix conditioner B^{>i}.

Main statements #

theorem

InformationTheory.Shannon.BroadcastChannel.mutualInfo_chain_rule_Y_fin_suffix

source
{Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {δ : Type u_2} [MeasurableSpace δ] [StandardBorelSpace δ] [Nonempty δ] {γ : Type u_3} [Fintype γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] [StandardBorelSpace γ] [Nonempty γ] (μ : 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 : { j : Fin n // ↑i < ↑j }) => Bs (↑j) ω

Chain rule for mutual information expanded along the sequence argument in reverse order: I(W; Bⁿ) = ∑ᵢ I(W; Bᵢ | B^{>i}), the conditioner being the suffix B^{>i}. The suffix counterpart of mutualInfo_chain_rule_Y_fin', obtained by reindexing the sequence with Fin.rev so that the prefix expansion applies and then transporting the resulting prefix conditioner back across that reindexing.

@audit:ok

Used by
    theorem

    InformationTheory.Shannon.BroadcastChannel.condMutualInfo_suffix_chain_rule_full

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

    Conditional chain rule expanded along the sequence in reverse order: I(Bⁿ; C | Z) = ∑ᵢ I(Bᵢ; C | (Z, B^{>i})), the background conditioner Z riding along untouched. Same Fin.rev reindexing as mutualInfo_chain_rule_Y_fin_suffix, applied to condMutualInfo_prefix_chain_rule; hZC is the finiteness side condition that expansion needs in order to cancel the background term I(Z; C).

    @audit:ok

    Used by
      theorem

      InformationTheory.Shannon.BroadcastChannel.condMutualInfo_le_add_condMutualInfo

      source
      {Ω : Type u_1} [MeasurableSpace Ω] {κ : Type u_2} [MeasurableSpace κ] [StandardBorelSpace κ] [Nonempty κ] {lam : Type u_3} [MeasurableSpace lam] [StandardBorelSpace lam] [Nonempty lam] {δ : Type u_4} [MeasurableSpace δ] [StandardBorelSpace δ] [Nonempty δ] {ζ : Type u_5} [MeasurableSpace ζ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (A : Ω → κ) (B : Ω → lam) (C : Ω → δ) (Z : Ω → ζ) (hA : Measurable A) (hB : Measurable B) (hC : Measurable C) (hZ : Measurable Z) (hZC : mutualInfo μ Z C ≠ ⊤) :
      condMutualInfo μ A C Z ≤ condMutualInfo μ B C Z + condMutualInfo μ A C fun (ω : Ω) => (Z ω, B ω)

      Inserting a variable into the conditioner: I(A; C | Z) ≤ I(B; C | Z) + I(A; C | (Z, B)). Expanding I((Z, A, B); C) by the chain rule in the two possible orders gives two decompositions that differ by the nonnegative term I(B; C | (Z, A)), and the inequality is what remains after dropping it. hZC cancels the background term I(Z; C) shared by both decompositions.

      @audit:ok

      Used by
        theorem

        InformationTheory.Shannon.BroadcastChannel.csiszar_sum_identity_cond

        source
        {Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {α : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [StandardBorelSpace α] [Nonempty α] {β : Type u_3} [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] [StandardBorelSpace β] [Nonempty β] {ξ : Type u_4} [Fintype ξ] [MeasurableSpace ξ] [MeasurableSingletonClass ξ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Wc : Ω → ξ) (As : Fin n → Ω → α) (Bs : Fin n → Ω → β) (hWc : Measurable Wc) (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 (ω : Ω) => (Wc ω, 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 (ω : Ω) => (Wc ω, fun (j : Fin ↑i) => As ⟨↑j, ⋯⟩ ω)

        Conditioned form of the Csiszár sum identity, for two sequences over distinct alphabets and a background conditioner Wc: ∑ᵢ I(A^{<i}; Bᵢ | (Wc, B^{>i})) = ∑ᵢ I(B^{>i}; Aᵢ | (Wc, A^{<i})). As in csiszar_sum_identity, both sides expand to the common triangular double sum ∑_{k<i} I(Aₖ; Bᵢ | (Wc, A^{<k}, B^{>i})) — the left by the prefix chain rule, the right by the suffix one — and the terms are matched by condMutualInfo_comm together with a prodComm relabel of the conditioner (El Gamal–Kim).

        @audit:ok

        Used by