InformationTheory.Shannon.BroadcastChannel.Marton.Achievability

Imports 5

Marton's inner bound — achievability #

The three-tier random-coding ensemble of Marton.ErrorAnalysis is assembled here into a single broadcast code. A rate pair strictly inside Marton's region is first split into subcodebook rates by exists_martonRateSplit; the covering lemma then makes the encoder's selection succeed with high probability, the conditional AEP of Marton.MarkovCore bounds the transmitted-pair term of each receiver, and the alias estimate bounds every other message row. A pigeonhole over the ensemble turns the averaged bound into one deterministic code.

Three radii are nested rather than shared: the decoders test weak joint typicality at radius ε, the transmitted blocks are pinned at martonStrongRadius, and the encoder selects a pair pinned at martonCoveringRadius, the smallest of the three. The two receivers induce unrelated covering radii, so the selection runs at their minimum and is reopened to either one by jointStronglyTypicalSet_mono_radius.

Main statements #

marton_achievability — a rate pair satisfying the three strict Marton inequalities is achievable over a general two-receiver broadcast channel.

Generic finite-sum plumbing #

Aggregating one receiver's Bonferroni decomposition over the ensemble #

The transmitted-pair term over the ensemble #

Per-receiver ensemble averages #

From the ensemble to one code #

Headline #

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.marton_achievability

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) {ε' : ℝ} (hε' : 0 < ε') :

∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ (M₁ : ℕ) (M₂ : ℕ) (_ : ⌈Real.exp (↑n * R₁)⌉₊ ≤ M₁) (_ : ⌈Real.exp (↑n * R₂)⌉₊ ≤ M₂) (c : BroadcastCode M₁ M₂ n α β₁ β₂), (c.averageErrorProb₁ W).toReal < ε' ∧ (c.averageErrorProb₂ W).toReal < ε'

Achievability of Marton's inner bound for a two-receiver broadcast channel with private messages. For auxiliary variables with joint law pV, an input kernel K and a channel W, a rate pair obeying the three strict inequalities

R₁ < I(V₁; Y₁),
R₂ < I(V₂; Y₂),
R₁ + R₂ < I(V₁; Y₁) + I(V₂; Y₂) − I(V₁; V₂)

is achievable: at every large enough block length there is a BroadcastCode whose two average error probabilities are both below any prescribed ε'.

The input is a general kernel K : Kernel (V₁ × V₂) α rather than a deterministic map x = f(v₁, v₂), so the textbook statement for a deterministic input is not a direct corollary: a deterministic kernel puts no mass on inputs off its image and therefore violates the full-support hypothesis hK that every typicality estimate in this development requires. The rate region is the same either way.

The hypotheses hpV, hK and hW are full-support regularity preconditions, shared with marton_strong_mutual_covering and with bc_achievability, and carry no part of the coding argument. No positivity of the rates is assumed: a nonpositive rate only asks for a single message, ⌈exp (n R)⌉₊ = 1, which the construction supplies as well.

No typicality radius appears in the statement, and the construction uses three nested ones rather than a single shared one: the two decoders test weak joint typicality at a radius ε, the transmitted blocks are pinned at the strictly smaller martonStrongRadius, and the encoder selects a pair pinned at the smaller martonCoveringRadius again.

@audit:ok

Used by