InformationTheory.Shannon.BroadcastChannel.OuterBoundUV

Imports 15

General broadcast channel — the UV outer bound (Nair–El Gamal) #

Single-letterization of the four information inequalities of the Nair–El Gamal outer bound for a general (not necessarily degraded) two-receiver broadcast channel, El Gamal–Kim. The bound reads

R₁ ≤ I(V; Y₁),                R₂ ≤ I(U; Y₂),
R₁ + R₂ ≤ I(U; Y₂) + I(X; Y₁ | U),
R₁ + R₂ ≤ I(V; Y₁) + I(X; Y₂ | V).

Both auxiliaries carry the same time structure uvAux, the receiver-1 output prefix together with the receiver-2 output suffix, and differ only in the message component: Uᵢ = (W₂, Y₁^{<i}, Y₂^{>i}) and Vᵢ = (W₁, Y₁^{<i}, Y₂^{>i}).

The two corner bounds are pure chain-rule plumbing and carry no structural hypothesis at all. The two sum bounds consume the Csiszár sum identity with a background conditioner (csiszar_sum_identity_cond) together with a memoryless precondition on the channel — the same h_memo bundle that the degraded converse takes. Unlike the degraded converse, no degradedness hypothesis appears: the conditioner swap that degradedness performed there is replaced here by the Csiszár identity, which is why the auxiliaries mix a prefix of one output with a suffix of the other.

Main definitions #

uvAux — the time structure shared by both auxiliaries: a message together with the receiver-1 output prefix and the receiver-2 output suffix.
InBCOuterRegionUV — the four inequalities of the bound, as a predicate on a rate pair and four abstract information slots.

Main statements #

bc_uv_singleletterize_r1 / bc_uv_singleletterize_r2 — the two corner bounds.
bc_uv_singleletterize_sum₂ / bc_uv_singleletterize_sum₁ — the two sum bounds.
bc_uv_converse — the four bounds at the message level, with the Fano slack.

The auxiliary variable #

def

InformationTheory.Shannon.BroadcastChannel.uvAux

source

{Ω : Type u_1} {n : ℕ} {ξ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (W : Ω → ξ) (Y₁s : Fin n → Ω → β₁) (Y₂s : Fin n → Ω → β₂) (i : Fin n) :

Ω → ξ × (Fin ↑i → β₁) × ({ j : Fin n // ↑i < ↑j } → β₂)

The auxiliary variable of the UV outer bound at letter i: a message together with the receiver-1 output prefix Y₁^{<i} and the receiver-2 output suffix Y₂^{>i}. Both auxiliaries of the bound have this shape and differ only in the message they carry — Uᵢ = uvAux W₂ … for the receiver-2 corner, Vᵢ = uvAux W₁ … for the receiver-1 one.

@audit:ok

Equations

InformationTheory.Shannon.BroadcastChannel.uvAux W Y₁s Y₂s i ω = (W ω, fun (j : Fin ↑i) => Y₁s ⟨↑j, ⋯⟩ ω, fun (j : { j : Fin n // ↑i < ↑j }) => Y₂s (↑j) ω)

Instances For

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.measurable_uvAux

source

{Ω : Type u_1} [MeasurableSpace Ω] {n : ℕ} {ξ : Type u_2} [MeasurableSpace ξ] {β₁ : Type u_3} [MeasurableSpace β₁] {β₂ : Type u_4} [MeasurableSpace β₂] (W : Ω → ξ) (Y₁s : Fin n → Ω → β₁) (Y₂s : Fin n → Ω → β₂) (hW : Measurable W) (hY₁s : ∀ (i : Fin n), Measurable (Y₁s i)) (hY₂s : ∀ (i : Fin n), Measurable (Y₂s i)) (i : Fin n) :

Measurable (uvAux W Y₁s Y₂s i)

Used by

Corner bounds #

theorem

InformationTheory.Shannon.BroadcastChannel.bc_uv_singleletterize_r1

source

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

(mutualInfo μ W₁ fun (ω : Ω) (j : Fin n) => Y₁s j ω) ≤ ∑ i : Fin n, mutualInfo μ (uvAux W₁ Y₁s Y₂s i) (Y₁s i)

Receiver-1 corner bound: with Vᵢ = uvAux W₁ Y₁s Y₂s i = (W₁, Y₁^{<i}, Y₂^{>i}), the message–output mutual information is dominated by the per-letter sum I(W₁; Y₁ⁿ) ≤ ∑ᵢ I(Vᵢ; Y_{1,i}). Nothing but measurability is assumed: expanding the left side along the prefix chain rule leaves ∑ᵢ I(W₁; Y_{1,i} | Y₁^{<i}), and adjoining first the prefix and then the receiver-2 suffix to the data variable only increases each summand.

@audit:ok

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.bc_uv_singleletterize_r2

source

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

(mutualInfo μ W₂ fun (ω : Ω) (j : Fin n) => Y₂s j ω) ≤ ∑ i : Fin n, mutualInfo μ (uvAux W₂ Y₁s Y₂s i) (Y₂s i)

Receiver-2 corner bound: with Uᵢ = uvAux W₂ Y₁s Y₂s i = (W₂, Y₁^{<i}, Y₂^{>i}), I(W₂; Y₂ⁿ) ≤ ∑ᵢ I(Uᵢ; Y_{2,i}). The mirror of bc_uv_singleletterize_r1, expanded along the reverse-order chain rule mutualInfo_chain_rule_Y_fin_suffix so that the conditioner it produces is the receiver-2 suffix the auxiliary already carries.

@audit:ok

Used by

Sum-rate bounds #

theorem

InformationTheory.Shannon.BroadcastChannel.bc_uv_singleletterize_sum₂

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 β₁] [StandardBorelSpace β₁] [Nonempty β₁] {β₂ : Type u_5} [Fintype β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] [StandardBorelSpace β₂] [Nonempty β₂] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (W₂ : Ω → ξ) (Xs : Fin n → Ω → α) (Y₁s : Fin n → Ω → β₁) (Y₂s : Fin n → Ω → β₂) (hW₂ : Measurable W₂) (hXs : ∀ (i : Fin n), Measurable (Xs i)) (hY₁s : ∀ (i : Fin n), Measurable (Y₁s i)) (hY₂s : ∀ (i : Fin n), Measurable (Y₂s i)) (h_memo : ∀ (i : Fin n), IsMarkovChain μ (fun (ω : Ω) => (W₂ ω, fun (j : { j : Fin n // j ≠ i }) => Xs (↑j) ω, fun (j : { j : Fin n // j ≠ i }) => Y₁s (↑j) ω, fun (j : { j : Fin n // j ≠ i }) => Y₂s (↑j) ω)) (Xs i) (Y₁s i)) :

(mutualInfo μ W₂ fun (ω : Ω) (j : Fin n) => Y₂s j ω) + condMutualInfo μ (fun (ω : Ω) (j : Fin n) => Xs j ω) (fun (ω : Ω) (j : Fin n) => Y₁s j ω) W₂ ≤ ∑ i : Fin n, (mutualInfo μ (uvAux W₂ Y₁s Y₂s i) (Y₂s i) + condMutualInfo μ (Xs i) (Y₁s i) (uvAux W₂ Y₁s Y₂s i))

Sum-rate single-letterization carrying the receiver-2 auxiliary in the leading term: I(W₂; Y₂ⁿ) + I(Xⁿ; Y₁ⁿ | W₂) ≤ ∑ᵢ (I(Uᵢ; Y_{2,i}) + I(Xᵢ; Y_{1,i} | Uᵢ)) for Uᵢ = (W₂, Y₁^{<i}, Y₂^{>i}). Two structural ingredients: the Csiszár sum identity with the background conditioner W₂ (csiszar_sum_identity_cond) trades the receiver-1 prefix terms left over by the chain-rule expansion for receiver-2 suffix terms the auxiliary absorbs, and h_memo — joint-output memorylessness Y_{1,i} ⫫ (W₂, X^{≠i}, Y₁^{≠i}, Y₂^{≠i}) | Xᵢ — collapses the full input Xⁿ to the single letter Xᵢ.

@audit:ok

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.bc_uv_singleletterize_sum₁

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 β₁] [StandardBorelSpace β₁] [Nonempty β₁] {β₂ : Type u_5} [Fintype β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] [StandardBorelSpace β₂] [Nonempty β₂] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (W₁ : Ω → ξ) (Xs : Fin n → Ω → α) (Y₁s : Fin n → Ω → β₁) (Y₂s : Fin n → Ω → β₂) (hW₁ : Measurable W₁) (hXs : ∀ (i : Fin n), Measurable (Xs i)) (hY₁s : ∀ (i : Fin n), Measurable (Y₁s i)) (hY₂s : ∀ (i : Fin n), Measurable (Y₂s i)) (h_memo : ∀ (i : Fin n), IsMarkovChain μ (fun (ω : Ω) => (W₁ ω, fun (j : { j : Fin n // j ≠ i }) => Xs (↑j) ω, fun (j : { j : Fin n // j ≠ i }) => Y₁s (↑j) ω, fun (j : { j : Fin n // j ≠ i }) => Y₂s (↑j) ω)) (Xs i) (Y₂s i)) :

(mutualInfo μ W₁ fun (ω : Ω) (j : Fin n) => Y₁s j ω) + condMutualInfo μ (fun (ω : Ω) (j : Fin n) => Xs j ω) (fun (ω : Ω) (j : Fin n) => Y₂s j ω) W₁ ≤ ∑ i : Fin n, (mutualInfo μ (uvAux W₁ Y₁s Y₂s i) (Y₁s i) + condMutualInfo μ (Xs i) (Y₂s i) (uvAux W₁ Y₁s Y₂s i))

Sum-rate single-letterization carrying the receiver-1 auxiliary in the leading term: I(W₁; Y₁ⁿ) + I(Xⁿ; Y₂ⁿ | W₁) ≤ ∑ᵢ (I(Vᵢ; Y_{1,i}) + I(Xᵢ; Y_{2,i} | Vᵢ)) for Vᵢ = (W₁, Y₁^{<i}, Y₂^{>i}). The mirror of bc_uv_singleletterize_sum₂: the Csiszár identity is consumed in the opposite direction, trading receiver-2 suffix terms for receiver-1 prefix terms, and h_memo is the memoryless hypothesis for the receiver-2 letter Y_{2,i}.

@audit:ok

Used by

Message level #

structure

InformationTheory.Shannon.BroadcastChannel.InBCOuterRegionUV

source

(R₁ R₂ I₁ I₂ J₂ J₁ : ℝ) :

Prop

The Nair–El Gamal (UV) outer-bound predicate: the two corner inequalities together with the two sum-rate inequalities. As with InBCCapacityRegion the four information slots are abstract; the intended instantiation (bc_uv_converse) is I₁ = ∑ᵢ I(Vᵢ; Y_{1,i}), I₂ = ∑ᵢ I(Uᵢ; Y_{2,i}), J₂ = ∑ᵢ (I(Uᵢ; Y_{2,i}) + I(Xᵢ; Y_{1,i} | Uᵢ)) and J₁ = ∑ᵢ (I(Vᵢ; Y_{1,i}) + I(Xᵢ; Y_{2,i} | Vᵢ)), each with the Fano slack added.

@audit:ok

bound₁ : R₁ ≤ I₁
Receiver-1 corner bound.
bound₂ : R₂ ≤ I₂
Receiver-2 corner bound.
sumBound₂ : R₁ + R₂ ≤ J₂
Sum-rate bound with the receiver-2 auxiliary in the leading term.
sumBound₁ : R₁ + R₂ ≤ J₁
Sum-rate bound with the receiver-1 auxiliary in the leading term.

Instances For

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.bc_uv_converse

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 ξ₂] [StandardBorelSpace ξ₂] [Nonempty ξ₂] {β₁ : Type u_5} [Fintype β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [StandardBorelSpace β₁] [Nonempty β₁] {β₂ : Type u_6} [Fintype β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] [StandardBorelSpace β₂] [Nonempty β₂] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (W₁ : Ω → ξ₁) (W₂ : Ω → ξ₂) (Xs : Fin n → Ω → α) (Y₁s : Fin n → Ω → β₁) (Y₂s : Fin n → Ω → β₂) (dec₁ : (Fin n → β₁) → ξ₁) (dec₂ : (Fin n → β₂) → ξ₂) (hW₁ : Measurable W₁) (hW₂ : Measurable W₂) (hXs : ∀ (j : Fin n), Measurable (Xs j)) (hY₁s : ∀ (j : Fin n), Measurable (Y₁s j)) (hY₂s : ∀ (j : Fin n), Measurable (Y₂s j)) (hW₁_uniform : MeasureTheory.Measure.map W₁ μ = (↑(Fintype.card ξ₁))⁻¹ • MeasureTheory.Measure.count) (hW₂_uniform : MeasureTheory.Measure.map W₂ μ = (↑(Fintype.card ξ₂))⁻¹ • MeasureTheory.Measure.count) (hcard₁ : 2 ≤ Fintype.card ξ₁) (hcard₂ : 2 ≤ Fintype.card ξ₂) (h_indep : mutualInfo μ W₁ W₂ = 0) (h_memo₁ : ∀ (i : Fin n), IsMarkovChain μ (fun (ω : Ω) => (W₂ ω, fun (j : { j : Fin n // j ≠ i }) => Xs (↑j) ω, fun (j : { j : Fin n // j ≠ i }) => Y₁s (↑j) ω, fun (j : { j : Fin n // j ≠ i }) => Y₂s (↑j) ω)) (Xs i) (Y₁s i)) (h_memo₂ : ∀ (i : Fin n), IsMarkovChain μ (fun (ω : Ω) => (W₁ ω, fun (j : { j : Fin n // j ≠ i }) => Xs (↑j) ω, fun (j : { j : Fin n // j ≠ i }) => Y₁s (↑j) ω, fun (j : { j : Fin n // j ≠ i }) => Y₂s (↑j) ω)) (Xs i) (Y₂s i)) (hmarkov₁ : IsMarkovChain μ (fun (ω : Ω) => (W₂ ω, W₁ ω)) (fun (ω : Ω) => (W₂ ω, fun (j : Fin n) => Xs j ω)) fun (ω : Ω) (j : Fin n) => Y₁s j ω) (hmarkov₂ : IsMarkovChain μ (fun (ω : Ω) => (W₁ ω, W₂ ω)) (fun (ω : Ω) => (W₁ ω, fun (j : Fin n) => Xs j ω)) fun (ω : Ω) (j : Fin n) => Y₂s j ω) :

InBCOuterRegionUV (Real.log ↑(Fintype.card ξ₁)) (Real.log ↑(Fintype.card ξ₂)) ((∑ i : Fin n, mutualInfo μ (uvAux W₁ Y₁s Y₂s i) (Y₁s i)).toReal + Real.binEntropy (MeasureFano.errorProb μ W₁ (fun (ω : Ω) (j : Fin n) => Y₁s j ω) dec₁) + MeasureFano.errorProb μ W₁ (fun (ω : Ω) (j : Fin n) => Y₁s j ω) dec₁ * Real.log (↑(Fintype.card ξ₁) - 1)) ((∑ i : Fin n, mutualInfo μ (uvAux W₂ Y₁s Y₂s i) (Y₂s i)).toReal + Real.binEntropy (MeasureFano.errorProb μ W₂ (fun (ω : Ω) (j : Fin n) => Y₂s j ω) dec₂) + MeasureFano.errorProb μ W₂ (fun (ω : Ω) (j : Fin n) => Y₂s j ω) dec₂ * Real.log (↑(Fintype.card ξ₂) - 1)) ((∑ i : Fin n, (mutualInfo μ (uvAux W₂ Y₁s Y₂s i) (Y₂s i) + condMutualInfo μ (Xs i) (Y₁s i) (uvAux W₂ Y₁s Y₂s i))).toReal + (Real.binEntropy (MeasureFano.errorProb μ W₁ (fun (ω : Ω) (j : Fin n) => Y₁s j ω) dec₁) + MeasureFano.errorProb μ W₁ (fun (ω : Ω) (j : Fin n) => Y₁s j ω) dec₁ * Real.log (↑(Fintype.card ξ₁) - 1)) + (Real.binEntropy (MeasureFano.errorProb μ W₂ (fun (ω : Ω) (j : Fin n) => Y₂s j ω) dec₂) + MeasureFano.errorProb μ W₂ (fun (ω : Ω) (j : Fin n) => Y₂s j ω) dec₂ * Real.log (↑(Fintype.card ξ₂) - 1))) ((∑ i : Fin n, (mutualInfo μ (uvAux W₁ Y₁s Y₂s i) (Y₁s i) + condMutualInfo μ (Xs i) (Y₂s i) (uvAux W₁ Y₁s Y₂s i))).toReal + (Real.binEntropy (MeasureFano.errorProb μ W₁ (fun (ω : Ω) (j : Fin n) => Y₁s j ω) dec₁) + MeasureFano.errorProb μ W₁ (fun (ω : Ω) (j : Fin n) => Y₁s j ω) dec₁ * Real.log (↑(Fintype.card ξ₁) - 1)) + (Real.binEntropy (MeasureFano.errorProb μ W₂ (fun (ω : Ω) (j : Fin n) => Y₂s j ω) dec₂) + MeasureFano.errorProb μ W₂ (fun (ω : Ω) (j : Fin n) => Y₂s j ω) dec₂ * Real.log (↑(Fintype.card ξ₂) - 1)))

Message-level UV outer bound for the general broadcast channel (El Gamal–Kim): for uniform, independent messages sent over a memoryless broadcast channel and decoded per receiver, the rate pair lies in the Nair–El Gamal region whose four information bounds are the per-letter sums over the auxiliaries Uᵢ = (W₂, Y₁^{<i}, Y₂^{>i}) and Vᵢ = (W₁, Y₁^{<i}, Y₂^{>i}), plus the Fano error slack.

No degradedness is assumed: what the degraded converse obtained from a conditioner swap is supplied here by the Csiszár sum identity. The remaining structural preconditions encode the channel, not the conclusion:

h_memo₁ / h_memo₂ — joint-output memoryless, Y_{k,i} ⫫ (W, X^{≠i}, Y₁^{≠i}, Y₂^{≠i}) | Xᵢ. The same-letter pair (Y_{1,i}, Y_{2,i}) is never decoupled, so the two outputs stay arbitrarily correlated within a letter.
hmarkov₁ / hmarkov₂ — the encoder Markov chain (W₂, W₁) → (W₂, Xⁿ) → Y₁ⁿ and its mirror, which is what makes the messages act on the outputs only through the codeword.

The operational instantiation — building μ from uniform messages through the encoder and the channel — is a separate wrapper, not part of this statement.

@audit:ok

Used by