InformationTheory.Shannon.BroadcastChannel.Operational

Imports 2

Broadcast channel — operational capacity region #

The operational capacity region of a general two-receiver broadcast channel, following the multiple-access template of InformationTheory.Shannon.MAC.macCapacityRegion: an operational achievability predicate on rate pairs, whose closure is taken as a subset of the plane, so that inner and outer bounds can be compared as sets.

Marton's inner bound, stated pointwise by InMartonRegion, is lifted to a subset of the plane here and shown to sit inside the operational region.

Main definitions #

BCAchievable W R₁ R₂ — the operational achievability predicate for the rate pair (R₁, R₂): for every target error ε' > 0, at every large enough block length there is a code with at least ⌈exp (n R₁)⌉ / ⌈exp (n R₂)⌉ messages per receiver whose two average error probabilities are both < ε'. This is the conclusion of marton_achievability, abstracted over ε'.
bcCapacityRegion W — the operational capacity region, the topological closure of the achievable set. (The achievable set is described by strict inequalities and is not closed, so the region is defined as its closure.)
martonRegion pV K W — Marton's inner bound as a subset of the plane, cut out by InMartonRegion for the three informations of the auxiliary law pV, input kernel K and channel W.

Main statements #

marton_region_subset_capacity — Marton's inner bound is contained in the operational capacity region.

def

InformationTheory.Shannon.BroadcastChannel.BCAchievable

source

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

Prop

The operational achievability predicate for the broadcast rate pair (R₁, R₂): for every target error ε' > 0 there is a block length N such that for all n ≥ N there is a length-n broadcast code with at least ⌈exp (n R₁)⌉ / ⌈exp (n R₂)⌉ messages per receiver whose two average error probabilities are both below ε'. This is the ∀ ε'-abstraction of the conclusion of marton_achievability.

Both message counts are at least one, since 1 ≤ ⌈exp (n R)⌉₊ at every real rate, so the degenerate M₁ * M₂ = 0 branch of averageErrorProb₁ — which reports an error probability of 0 — is out of reach: an empty code cannot witness achievability. @audit:ok

Equations

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

Instances For

Used by

def

InformationTheory.Shannon.BroadcastChannel.bcCapacityRegion

source

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

Set (ℝ × ℝ)

The operational broadcast capacity region: the topological closure of the achievable set. The achievable set is cut out by strict inequalities and is not closed (boundary faces enter only in the closure), so the capacity region is defined as its closure.

The region is a down-set of the whole plane rather than of the first quadrant, since a nonpositive rate asks only for a single message and is achievable. An outer bound should therefore be stated without a sign constraint, or compared after intersecting with the first quadrant. @audit:ok

Equations

InformationTheory.Shannon.BroadcastChannel.bcCapacityRegion W = closure {p : ℝ × ℝ | InformationTheory.Shannon.BroadcastChannel.BCAchievable W p.1 p.2}

Instances For

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.bc_achievable_mono

source

{α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [MeasurableSpace α] [MeasurableSpace β₁] [MeasurableSpace β₂] {W : BCChannel α β₁ β₂} {R₁ R₂ R₁' R₂' : ℝ} (h : BCAchievable W R₁ R₂) (h₁ : R₁' ≤ R₁) (h₂ : R₂' ≤ R₂) :

BCAchievable W R₁' R₂'

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.bc_mem_closure_of_strictly_below

source

{α : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} [MeasurableSpace α] [MeasurableSpace β₁] [MeasurableSpace β₂] (W : BCChannel α β₁ β₂) (p : ℝ × ℝ) (h : ∀ (ε : ℝ), 0 < ε → BCAchievable W (p.1 - ε) (p.2 - ε)) :

p ∈ closure {q : ℝ × ℝ | BCAchievable W q.1 q.2}

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.bc_capacityRegion_isClosed

source

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

IsClosed (bcCapacityRegion W)

Used by

def

InformationTheory.Shannon.BroadcastChannel.Marton.martonRegion

source

{V₁ : Type u_1} {V₂ : Type u_2} {α : Type u_3} {β₁ : Type u_4} {β₂ : Type u_5} [Fintype V₁] [MeasurableSpace V₁] [Fintype V₂] [MeasurableSpace V₂] [MeasurableSpace α] [Fintype β₁] [MeasurableSpace β₁] [Fintype β₂] [MeasurableSpace β₂] (pV : MeasureTheory.Measure (V₁ × V₂)) (K : ProbabilityTheory.Kernel (V₁ × V₂) α) (W : BCChannel α β₁ β₂) :

Set (ℝ × ℝ)

Marton's inner bound as a subset of the plane: the rate pairs satisfying the three inequalities of InMartonRegion for the informations martonInfo₁, martonInfo₂ and martonInfoV₁V₂ of the auxiliary law pV, input kernel K and channel W. This is the region of one fixed choice of pV, K and W; the union over auxiliary alphabets is not taken.

Like bcCapacityRegion and the outer bounds, the region carries no sign constraint: a nonpositive rate asks only for a single message and is achievable, so cutting the bound down to the first quadrant would place it strictly inside the capacity region for no gain and would break every comparison against a region of the whole plane. @audit:ok

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.bc_strict_interior_achievable

source

{V₁ : Type u_1} {V₂ : Type u_2} {α : Type u_3} {β₁ : Type u_4} {β₂ : Type u_5} [Fintype V₁] [DecidableEq V₁] [Nonempty V₁] [MeasurableSpace V₁] [MeasurableSingletonClass V₁] [Fintype V₂] [DecidableEq V₂] [Nonempty V₂] [MeasurableSpace V₂] [MeasurableSingletonClass V₂] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [DecidableEq β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [DecidableEq β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (pV : MeasureTheory.Measure (V₁ × V₂)) [MeasureTheory.IsProbabilityMeasure pV] (K : ProbabilityTheory.Kernel (V₁ × V₂) α) [ProbabilityTheory.IsMarkovKernel K] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (hpV : ∀ (v : V₁ × V₂), 0 < pV.real {v}) (hK : ∀ (v : V₁ × V₂) (a : α), 0 < (K v).real {a}) (hW : ∀ (a : α) (b : β₁ × β₂), 0 < (W a).real {b}) {R₁ R₂ : ℝ} (hR₁lt : R₁ < martonInfo₁ pV K W) (hR₂lt : R₂ < martonInfo₂ pV K W) (hRsum : R₁ + R₂ < martonInfo₁ pV K W + martonInfo₂ pV K W - martonInfoV₁V₂ pV K W) :

BCAchievable W R₁ R₂

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.marton_region_subset_capacity

source

martonRegion pV K W ⊆ bcCapacityRegion W

Marton's inner bound sits inside the operational capacity region. A rate pair of the region satisfies the three region inequalities non-strictly, so shrinking both rates by any ε > 0 makes all three strict and marton_achievability applies; letting ε tend to 0 recovers the pair in the closure.

The hypotheses hpV, hK and hW are the full-support regularity preconditions of marton_achievability and carry no part of the coding argument. The shrunk pair may leave the first quadrant, which costs nothing: a nonpositive rate asks only for a single message. @audit:ok

Used by