InformationTheory.Shannon.BroadcastChannel.Marton.Basic

Imports 3

Rate region of Marton's inner bound #

Marton's inner bound for a two-receiver broadcast channel with private messages is cut out by three inequalities on a rate pair (R₁, R₂), stated here over abstract information bounds I₁, I₂, I₁₂ standing for I(V₁; Y₁), I(V₂; Y₂) and I(V₁; V₂).

The random coding scheme behind the bound attaches to every message a subcodebook, of rate R₁' for the first receiver and R₂' for the second, so the three region inequalities are traded for one covering constraint I₁₂ < R₁' + R₂' together with two decoding constraints R₁ + R₁' < I₁ and R₂ + R₂' < I₂. Eliminating the subcodebook rates from that system recovers the region, and exists_martonRateSplit is the converse direction of the elimination.

Main definitions #

InMartonRegion R₁ R₂ I₁ I₂ I₁₂ — the three inequalities cutting out the region.

Main statements #

exists_martonRateSplit — a rate pair satisfying the three inequalities strictly admits a splitting into positive subcodebook rates meeting the covering and decoding constraints.

structure

InformationTheory.Shannon.BroadcastChannel.Marton.InMartonRegion

source

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

Prop

Marton's inner-bound region for a two-receiver broadcast channel with private messages: a bundle of the two corner inequalities R₁ ≤ I₁, R₂ ≤ I₂ and the sum-rate inequality R₁ + R₂ ≤ I₁ + I₂ - I₁₂ on five real numbers. The slots I₁, I₂, I₁₂ are abstract information bounds — the predicate does not fix their meaning, the intended instantiation being I₁ = I(V₁; Y₁), I₂ = I(V₂; Y₂) and I₁₂ = I(V₁; V₂) for a pair of auxiliary variables (V₁, V₂).

Taking I₁₂ = 0 degenerates the sum-rate inequality into the one implied by the two corner inequalities, so independent auxiliary variables give back the rectangular region of InformationTheory.Shannon.BroadcastChannel.InBCCapacityRegion.

bound₁ : R₁ ≤ I₁
Receiver-1 rate bound.
bound₂ : R₂ ≤ I₂
Receiver-2 rate bound.
boundSum : R₁ + R₂ ≤ I₁ + I₂ - I₁₂
Sum-rate bound, discounted by the dependence between the auxiliary variables.

Instances For

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.InMartonRegion.mono

source

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

InMartonRegion R₁ R₂ I₁' I₂' I₁₂'

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.exists_martonRateSplit

source

{R₁ R₂ I₁ I₂ I₁₂ : ℝ} (h₁ : R₁ < I₁) (h₂ : R₂ < I₂) (hsum : R₁ + R₂ < I₁ + I₂ - I₁₂) :

∃ (R₁' : ℝ) (R₂' : ℝ), 0 < R₁' ∧ 0 < R₂' ∧ I₁₂ < R₁' + R₂' ∧ R₁ + R₁' < I₁ ∧ R₂ + R₂' < I₂

Splitting of a strictly interior rate pair into subcodebook rates: the three strict Marton inequalities produce positive rates R₁', R₂' whose sum exceeds I₁₂ while each message rate still leaves room for its subcodebook, R₁ + R₁' < I₁ and R₂ + R₂' < I₂. This is the direction of the Fourier–Motzkin elimination that the coding scheme consumes; the reverse direction, that such a splitting forces the three inequalities, is immediate. Positivity rather than nonnegativity is what the covering step needs: it sizes the selection radius by a fraction of each subcodebook rate, which a rate of zero leaves no room for.

@audit:ok

Used by