InformationTheory.Shannon.BroadcastChannel.Basic

Imports 3

Broadcast channel — primitive definitions #

Two-receiver broadcast channel (BC) primitives, following the single-user InformationTheory.Shannon.ChannelCoding.Basic and the multiple-access InformationTheory.Shannon.MultipleAccess.Basic conventions (Cover–Thomas).

Main definitions #

BCChannel α β₁ β₂ := Kernel α (β₁ × β₂) — a discrete BC with one input and a pair of outputs.
IsBCDegraded W — physical degradedness X → Y₁ → Y₂: the second output is the first one passed through a further kernel.
BroadcastCode M₁ M₂ n α β₁ β₂ — a two-receiver block code: one joint encoder for the message pair and a separate decoder per receiver.
BroadcastCode.errorProbAt₁ / errorProbAt₂ — the pointwise per-receiver block-decoding error probabilities.
BroadcastCode.padFirst, BroadcastCode.padSecond — a second message attached to a receiver that carries only one, which is what brings a code of a zero rate into the scope of a converse asking for at least two messages per receiver.
InBCCapacityRegion R₁ R₂ I₁ I₂ — the auxiliary-variable capacity-region predicate bundling the two corner inequalities R₁ ≤ I₁, R₂ ≤ I₂ (degraded BC, Cover–Thomas: I₁ = I(X; Y₁ | U), I₂ = I(U; Y₂)).

abbrev

InformationTheory.Shannon.BroadcastChannel.BCChannel

source

@[reducible, inline]

(α : Type u_4) (β₁ : Type u_5) (β₂ : Type u_6) [MeasurableSpace α] [MeasurableSpace β₁] [MeasurableSpace β₂] :

Type (max u_4 u_6 u_5)

A discrete broadcast channel: a Markov kernel from the input α to the output pair β₁ × β₂ (receiver 1 sees the first coordinate, receiver 2 the second).

Equations

InformationTheory.Shannon.BroadcastChannel.BCChannel α β₁ β₂ = ProbabilityTheory.Kernel α (β₁ × β₂)

Instances For

Used by

def

InformationTheory.Shannon.BroadcastChannel.IsBCDegraded

source

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

Prop

Physical degradedness X → Y₁ → Y₂: the second (degraded) output is a stochastic function of the first output alone. There is a Markov kernel Q : Kernel β₁ β₂ (the degrading channel) such that sampling (y₁, y₂) ∼ W x is the same as sampling y₁ ∼ (W x).map Prod.fst and then y₂ ∼ Q y₁. A condition on the channel alone, constraining neither the code nor the input law: it is a structural precondition rather than a load-bearing hypothesis, and the block-prefix degradedness the converse runs on is derived from it.

Equations

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

Instances For

Used by

structure

InformationTheory.Shannon.BroadcastChannel.BroadcastCode

source

(M₁ M₂ n : ℕ) (α : Type u_4) (β₁ : Type u_5) (β₂ : Type u_6) [MeasurableSpace α] [MeasurableSpace β₁] [MeasurableSpace β₂] :

Type (max (max u_4 u_5) u_6)

A two-receiver BC block code of length n: a joint encoder for the message pair and a separate decoder for each receiver. As in the single-user Code, no measurability fields are bundled (all functions on finite alphabets are automatically measurable).

encoder : Fin M₁ × Fin M₂ → Fin n → α
Joint encoder of the message pair into an input codeword.
decoder₁ : (Fin n → β₁) → Fin M₁
Decoder for receiver 1 (sees only the β₁ outputs).
decoder₂ : (Fin n → β₂) → Fin M₂
Decoder for receiver 2 (sees only the β₂ outputs).

Instances For

Used by

noncomputable def

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.blockOutputLaw

source

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

MeasureTheory.Measure (Fin n → β₁ × β₂)

Memoryless block output law for the message pair m: each letter i is sent through the channel W (encoder m i), with letters independent.

Equations

c.blockOutputLaw W m = MeasureTheory.Measure.pi fun (i : Fin n) => W (c.encoder m i)

Instances For

Used by

def

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.errorEvent₁

source

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

Set (Fin n → β₁ × β₂)

Receiver-1 error event for the pair m: outputs whose β₁-projection decodes to something other than m.1.

Equations

c.errorEvent₁ m = {y : Fin n → β₁ × β₂ | (c.decoder₁ fun (i : Fin n) => (y i).1) ≠ m.1}

Instances For

Used by

def

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.errorEvent₂

source

Set (Fin n → β₁ × β₂)

Receiver-2 error event for the pair m: outputs whose β₂-projection decodes to something other than m.2.

Equations

c.errorEvent₂ m = {y : Fin n → β₁ × β₂ | (c.decoder₂ fun (i : Fin n) => (y i).2) ≠ m.2}

Instances For

Used by

noncomputable def

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.errorProbAt₁

source

ENNReal

Pointwise receiver-1 error probability when the pair m is sent.

Equations

c.errorProbAt₁ W m = (c.blockOutputLaw W m) (c.errorEvent₁ m)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.errorProbAt₂

source

ENNReal

Pointwise receiver-2 error probability when the pair m is sent.

Equations

c.errorProbAt₂ W m = (c.blockOutputLaw W m) (c.errorEvent₂ m)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.averageErrorProb₁

source

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

ENNReal

Average receiver-1 error probability under a uniform message pair. For M₁·M₂ = 0 we set this to 0.

Equations

c.averageErrorProb₁ W = if M₁ * M₂ = 0 then 0 else (↑(M₁ * M₂))⁻¹ * ∑ m : Fin M₁ × Fin M₂, c.errorProbAt₁ W m

Instances For

Used by

noncomputable def

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.averageErrorProb₂

source

ENNReal

Average receiver-2 error probability under a uniform message pair. For M₁·M₂ = 0 we set this to 0.

Equations

c.averageErrorProb₂ W = if M₁ * M₂ = 0 then 0 else (↑(M₁ * M₂))⁻¹ * ∑ m : Fin M₁ × Fin M₂, c.errorProbAt₂ W m

Instances For

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.errorProbAt₁_le_one

source

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

c.errorProbAt₁ W m ≤ 1

Each pointwise receiver-1 error probability is at most 1.

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.errorProbAt₂_le_one

source

c.errorProbAt₂ W m ≤ 1

Each pointwise receiver-2 error probability is at most 1.

Used by

Padding a code that carries a single message #

def

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.padFirst

source

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

BroadcastCode 2 M₂ n α β₁ β₂

A second receiver-1 message attached to a code that carries only one. Both messages are sent with the single codeword of the original code, so receiver 1 cannot separate them, while receiver 2 sees exactly the original code. This is what puts a code of a nonpositive rate pair inside the scope of the converse, which asks for at least two messages per receiver. @audit:ok

Equations

c.padFirst = { encoder := fun (m : Fin 2 × Fin M₂) => c.encoder (0, m.2), decoder₁ := fun (x : Fin n → β₁) => 0, decoder₂ := c.decoder₂ }

Instances For

Used by

def

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.padSecond

source

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

BroadcastCode M₁ 2 n α β₁ β₂

The mirror of padFirst at the second receiver. @audit:ok

Equations

c.padSecond = { encoder := fun (m : Fin M₁ × Fin 2) => c.encoder (m.1, 0), decoder₁ := c.decoder₁, decoder₂ := fun (x : Fin n → β₂) => 0 }

Instances For

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.averageErrorProb₂_padFirst

source

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

c.padFirst.averageErrorProb₂ W = c.averageErrorProb₂ W

@audit:ok

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.BroadcastCode.averageErrorProb₁_padSecond

source

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

c.padSecond.averageErrorProb₁ W = c.averageErrorProb₁ W

@audit:ok

Used by

Auxiliary-variable capacity region (degraded BC) #

structure

InformationTheory.Shannon.BroadcastChannel.InBCCapacityRegion

source

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

Prop

The degraded-BC capacity-region predicate: a bundle of the two corner inequalities R₁ ≤ I₁, R₂ ≤ I₂ on four real numbers. The slots I₁, I₂ are abstract information bounds — the predicate does not fix their meaning. Two instantiations are intended:

message level (bc_converse_message_level): I₁ = I(W₁; (W₂, Y₁ⁿ)), I₂ = I(W₂; Y₂ⁿ) plus Fano terms.
single letter (the standard Cover–Thomas form, bc_degraded_converse): with an auxiliary U, I₁ = ∑ᵢ I(Xᵢ; Y_{1,i} | Uᵢ), I₂ = ∑ᵢ I(Uᵢ; Y_{2,i}).

Unlike the symmetric MAC region, the two receivers are asymmetric (receiver 2 is the degraded one), so there is no role-swap symmetry — only monotonicity in the information bounds (InBCCapacityRegion.mono).

bound₁ : R₁ ≤ I₁
Receiver-1 (strong) rate bound.
bound₂ : R₂ ≤ I₂
Receiver-2 (degraded) rate bound.

Instances For

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.InBCCapacityRegion.mono

source

{R₁ R₂ I₁ I₂ I₁' I₂' : ℝ} (h : InBCCapacityRegion R₁ R₂ I₁ I₂) (h₁ : I₁ ≤ I₁') (h₂ : I₂ ≤ I₂') :

InBCCapacityRegion R₁ R₂ I₁' I₂'

Monotonicity of the region in the information bounds: enlarging I₁, I₂ keeps the rate pair inside. This is the bridge from the message-level form to the single-letter form.

Used by