Skip to content

InformationTheory.Shannon.BroadcastChannel.OuterBound

Imports 4

Broadcast channel — cooperative outer bound #

An outer bound on the operational capacity region of a general two-receiver broadcast channel, obtained by letting the two receivers cooperate. Each receiver alone, and the two receivers pooling their outputs, form single-user channels, so the single-user converse applies three times and bounds the two individual rates and their sum by the corresponding capacities.

The reductions are code transformations: freezing one message index turns a broadcast code into a single-user code for the other receiver over the marginal channel, and pairing the two message indices turns it into a single-user code over the channel with the output pair as its output.

Main definitions #

BroadcastCode.restrict₁ / BroadcastCode.restrict₂ — the single-user code obtained by freezing the message of the other receiver.
BroadcastCode.coop — the single-user code for the cooperative receiver that sees both outputs and decodes the message pair.
bcOuterRegionCoop W — the cooperative outer region, the intersection of the three half planes cut out by the capacities of the two marginal channels and of the channel itself.

Main statements #

bc_capacity_subset_coop — the operational capacity region is contained in the cooperative outer region.

def

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.restrict₁

{M₁ M₂ n : ℕ} {α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [MeasurableSpace α] [MeasurableSpace β₁] [MeasurableSpace β₂] (c : BroadcastCode M₁ M₂ n α β₁ β₂) (m₂ : Fin M₂) :

ChannelCoding.Code M₁ n α β₁

The single-user code for receiver 1 obtained from a broadcast code by freezing the message of receiver 2: the encoder sends the receiver-1 message paired with the frozen index, and the decoder is the receiver-1 decoder.

Equations

c.restrict₁ m₂ = { encoder := fun (m₁ : Fin M₁) => c.encoder (m₁, m₂), decoder := c.decoder₁ }

Instances For

Used by

def

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.restrict₂

{M₁ M₂ n : ℕ} {α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [MeasurableSpace α] [MeasurableSpace β₁] [MeasurableSpace β₂] (c : BroadcastCode M₁ M₂ n α β₁ β₂) (m₁ : Fin M₁) :

ChannelCoding.Code M₂ n α β₂

The single-user code for receiver 2 obtained from a broadcast code by freezing the message of receiver 1.

Equations

c.restrict₂ m₁ = { encoder := fun (m₂ : Fin M₂) => c.encoder (m₁, m₂), decoder := c.decoder₂ }

Instances For

Used by

def

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.coop

{M₁ M₂ n : ℕ} {α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [MeasurableSpace α] [MeasurableSpace β₁] [MeasurableSpace β₂] (c : BroadcastCode M₁ M₂ n α β₁ β₂) :

ChannelCoding.Code (M₁ * M₂) n α (β₁ × β₂)

The single-user code for the cooperative receiver: one message for the pair, and a decoder that runs both broadcast decoders on their own output coordinate and pairs the answers.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.errorProbAt_restrict₁

{M₁ M₂ n : ℕ} {α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [MeasurableSpace α] [Fintype β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [MeasurableSpace β₂] (c : BroadcastCode M₁ M₂ n α β₁ β₂) (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (m₁ : Fin M₁) (m₂ : Fin M₂) :

(c.restrict₁ m₂).errorProbAt (ProbabilityTheory.Kernel.fst W) m₁ = c.errorProbAt₁ W (m₁, m₂)

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.errorProbAt_restrict₂

{M₁ M₂ n : ℕ} {α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [MeasurableSpace α] [MeasurableSpace β₁] [Fintype β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (c : BroadcastCode M₁ M₂ n α β₁ β₂) (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (m₁ : Fin M₁) (m₂ : Fin M₂) :

(c.restrict₂ m₁).errorProbAt (ProbabilityTheory.Kernel.snd W) m₂ = c.errorProbAt₂ W (m₁, m₂)

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.errorProbAt_coop_le

{M₁ M₂ n : ℕ} {α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [MeasurableSpace α] [MeasurableSpace β₁] [MeasurableSpace β₂] (c : BroadcastCode M₁ M₂ n α β₁ β₂) (W : BCChannel α β₁ β₂) (m : Fin (M₁ * M₂)) :

c.coop.errorProbAt W m ≤ c.errorProbAt₁ W (finProdFinEquiv.symm m) + c.errorProbAt₂ W (finProdFinEquiv.symm m)

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.averageErrorProb₁_le_one

{M₁ M₂ n : ℕ} {α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [MeasurableSpace α] [MeasurableSpace β₁] [MeasurableSpace β₂] (c : BroadcastCode M₁ M₂ n α β₁ β₂) (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] :

c.averageErrorProb₁ W ≤ 1

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.averageErrorProb₂_le_one

{M₁ M₂ n : ℕ} {α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [MeasurableSpace α] [MeasurableSpace β₁] [MeasurableSpace β₂] (c : BroadcastCode M₁ M₂ n α β₁ β₂) (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] :

c.averageErrorProb₂ W ≤ 1

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.exists_averageErrorProb_restrict₁_le

{M₁ M₂ n : ℕ} {α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [MeasurableSpace α] [Fintype β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [MeasurableSpace β₂] (c : BroadcastCode M₁ M₂ n α β₁ β₂) (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (hM₁ : 0 < M₁) (hM₂ : 0 < M₂) :

∃ (m₂ : Fin M₂), (c.restrict₁ m₂).averageErrorProb (ProbabilityTheory.Kernel.fst W) ≤ c.averageErrorProb₁ W

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.exists_averageErrorProb_restrict₂_le

{M₁ M₂ n : ℕ} {α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [MeasurableSpace α] [MeasurableSpace β₁] [Fintype β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (c : BroadcastCode M₁ M₂ n α β₁ β₂) (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (hM₁ : 0 < M₁) (hM₂ : 0 < M₂) :

∃ (m₁ : Fin M₁), (c.restrict₂ m₁).averageErrorProb (ProbabilityTheory.Kernel.snd W) ≤ c.averageErrorProb₂ W

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.averageErrorProb_coop_le

{M₁ M₂ n : ℕ} {α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [MeasurableSpace α] [MeasurableSpace β₁] [MeasurableSpace β₂] (c : BroadcastCode M₁ M₂ n α β₁ β₂) (W : BCChannel α β₁ β₂) :

c.coop.averageErrorProb W ≤ c.averageErrorProb₁ W + c.averageErrorProb₂ W

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.bc_rate₁_le_capacity_fst

{α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [MeasurableSpace β₂] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (p : α → ℝ) (hp : p ∈ stdSimplex ℝ α) (hp_max : IsMaxOn (fun (q : α → ℝ) => (ChannelCoding.mutualInfoOfChannel (ChannelCoding.pmfToMeasure q) (ProbabilityTheory.Kernel.fst W)).toReal) (stdSimplex ℝ α) p) (hq_pos : ∀ (b : β₁), 0 < (ChannelCoding.outputDistribution (ChannelCoding.pmfToMeasure p) (ProbabilityTheory.Kernel.fst W)).real {b}) {R₁ R₂ : ℝ} (hach : BCAchievable W R₁ R₂) :

R₁ ≤ ChannelCoding.capacity (ProbabilityTheory.Kernel.fst W)

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.bc_rate₂_le_capacity_snd

{α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace β₁] [Fintype β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (p : α → ℝ) (hp : p ∈ stdSimplex ℝ α) (hp_max : IsMaxOn (fun (q : α → ℝ) => (ChannelCoding.mutualInfoOfChannel (ChannelCoding.pmfToMeasure q) (ProbabilityTheory.Kernel.snd W)).toReal) (stdSimplex ℝ α) p) (hq_pos : ∀ (b : β₂), 0 < (ChannelCoding.outputDistribution (ChannelCoding.pmfToMeasure p) (ProbabilityTheory.Kernel.snd W)).real {b}) {R₁ R₂ : ℝ} (hach : BCAchievable W R₁ R₂) :

R₂ ≤ ChannelCoding.capacity (ProbabilityTheory.Kernel.snd W)

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.bc_sum_rate_le_capacity

{α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (p : α → ℝ) (hp : p ∈ stdSimplex ℝ α) (hp_max : IsMaxOn (fun (q : α → ℝ) => (ChannelCoding.mutualInfoOfChannel (ChannelCoding.pmfToMeasure q) W).toReal) (stdSimplex ℝ α) p) (hq_pos : ∀ (b : β₁ × β₂), 0 < (ChannelCoding.outputDistribution (ChannelCoding.pmfToMeasure p) W).real {b}) {R₁ R₂ : ℝ} (hach : BCAchievable W R₁ R₂) :

R₁ + R₂ ≤ ChannelCoding.capacity W

Used by

def

InformationTheory.Shannon.BroadcastChannel.bcOuterRegionCoop

{α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [Fintype α] [MeasurableSpace α] [MeasurableSpace β₁] [MeasurableSpace β₂] (W : BCChannel α β₁ β₂) :

Set (ℝ × ℝ)

The cooperative outer region: the rate pairs whose two coordinates are bounded by the capacities of the two marginal channels and whose sum is bounded by the capacity of the channel read with the output pair as a single output.

No sign constraint is imposed. The operational region genuinely contains nonpositive rate pairs, which a single-message code achieves, so a first-quadrant outer region would not contain it; the three capacities are nonnegative, so the nonpositive part causes no loss.

The region is proper rather than the whole plane: each capacity is the supremum of a nonempty family of mutual informations bounded by log |α| + log |β|, so the three half planes cut at finite heights. @audit:ok

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.bcOuterRegionCoop_isClosed

{α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [Fintype α] [MeasurableSpace α] [MeasurableSpace β₁] [MeasurableSpace β₂] (W : BCChannel α β₁ β₂) :

IsClosed (bcOuterRegionCoop W)

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.bc_capacity_subset_coop

{α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (p₁ : α → ℝ) (hp₁ : p₁ ∈ stdSimplex ℝ α) (hp₁_max : IsMaxOn (fun (q : α → ℝ) => (ChannelCoding.mutualInfoOfChannel (ChannelCoding.pmfToMeasure q) (ProbabilityTheory.Kernel.fst W)).toReal) (stdSimplex ℝ α) p₁) (hq₁_pos : ∀ (b : β₁), 0 < (ChannelCoding.outputDistribution (ChannelCoding.pmfToMeasure p₁) (ProbabilityTheory.Kernel.fst W)).real {b}) (p₂ : α → ℝ) (hp₂ : p₂ ∈ stdSimplex ℝ α) (hp₂_max : IsMaxOn (fun (q : α → ℝ) => (ChannelCoding.mutualInfoOfChannel (ChannelCoding.pmfToMeasure q) (ProbabilityTheory.Kernel.snd W)).toReal) (stdSimplex ℝ α) p₂) (hq₂_pos : ∀ (b : β₂), 0 < (ChannelCoding.outputDistribution (ChannelCoding.pmfToMeasure p₂) (ProbabilityTheory.Kernel.snd W)).real {b}) (p₀ : α → ℝ) (hp₀ : p₀ ∈ stdSimplex ℝ α) (hp₀_max : IsMaxOn (fun (q : α → ℝ) => (ChannelCoding.mutualInfoOfChannel (ChannelCoding.pmfToMeasure q) W).toReal) (stdSimplex ℝ α) p₀) (hq₀_pos : ∀ (b : β₁ × β₂), 0 < (ChannelCoding.outputDistribution (ChannelCoding.pmfToMeasure p₀) W).real {b}) :

bcCapacityRegion W ⊆ bcOuterRegionCoop W

The operational capacity region of a general broadcast channel is contained in the cooperative outer region: letting the two receivers pool their outputs can only enlarge the set of achievable rate pairs, and the resulting single-user converses bound each rate and the sum.

The three capacity achievers and their full-support output preconditions are those of channelCoding_operational_rate_le_capacity, one set per single-user channel; none of them carries a part of the converse argument. The achievers cost nothing, since exists_capacity_achiever produces one for each of the three channels. @audit:ok

Used by