InformationTheory.Shannon.BroadcastChannel.Superposition.Assembly

Imports 2

Broadcast channel — the UV outer region of a less noisy channel is achievable #

The UV outer region is indexed by five-tuple laws whose auxiliaries range over a countable alphabet, the superposition inner bound by achievability pairs over a finite one. Truncating the first auxiliary at a level m moves a law of the outer region onto a finite alphabet at a cost the tail alone carries, and perturbing the achievability pair it yields toward the uniform law repairs that pair's support at a cost any positive slack covers.

The truncation leaves the corner slot of the first receiver alone, because that slot reads the second auxiliary, so the whole cost of the truncation is charged to the second rate once, and the same subtraction pays for the sum-rate constraint as well. The perturbation slack is subtracted from both rates. Neither cost depends on the other, so both vanish along one sequence of indices, and the inner bound is a closure, which recovers the rate pair itself from the shifted ones. Combined with the outer bound and with the achievability of the inner one, this describes the capacity region of a less noisy broadcast channel by a single-letter expression. Positive mass on every output pair is asked for by the achievability step alone; the inclusion of the outer region in the inner bound needs nothing beyond the less noisy hypothesis.

Main statements #

bc_lessNoisy_capacity_eq_uv — the single-letter characterization: the capacity region of a less noisy broadcast channel whose transition law gives every output pair positive mass is its UV outer region bcOuterRegionUV.
bc_lessNoisy_superposition_eq_capacity — the same capacity region read off the two-constraint superposition inner bound instead of the outer bound.
bc_lessNoisy_uv_subset_superposition — the inclusion the two equalities rest on: the UV outer region of a less noisy channel is contained in the two-constraint superposition inner bound over the full-support achievability pairs.

The reverse inclusion #

theorem

InformationTheory.Shannon.BroadcastChannel.uvInfo₂_toReal_sub_slack_le

source

{α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂)) [MeasureTheory.IsProbabilityMeasure ν] (m : ℕ) :

(uvInfo₂ ν).toReal - (uvQuantizeSlack ν m).toReal ≤ (uvInfo₂ (uvQuantizeLaw ν m)).toReal

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.uvInfoSum₂_toReal_sub_slack_le

source

{α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [StandardBorelSpace α] [Fintype β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [StandardBorelSpace β₁] [Fintype β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] {ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂)} [MeasureTheory.IsProbabilityMeasure ν] (h : IsUVChannelLaw W ν) (m : ℕ) :

(uvInfoSum₂ ν).toReal - (uvQuantizeSlack ν m).toReal ≤ (uvInfoSum₂ (uvQuantizeLaw ν m)).toReal

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.sub_mem_bcSuperpositionRegionNoSumRate_of_mem_uvRegion

source

{α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [StandardBorelSpace α] [Fintype β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [StandardBorelSpace β₁] [Fintype β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] [StandardBorelSpace β₂] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (hln : IsBCLessNoisy W) {ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂)} [MeasureTheory.IsProbabilityMeasure ν] (h : IsUVChannelLaw W ν) {p : ℝ × ℝ} (hp : p ∈ uvRegion ν) (m : ℕ) {δ : ℝ} (hδ : 0 < δ) :

(p.1 - δ, p.2 - (uvQuantizeSlack ν m).toReal - δ) ∈ bcSuperpositionRegionNoSumRate W

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.mem_bcSuperpositionRegionNoSumRate_of_mem_uvRegion

source

{α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [StandardBorelSpace α] [Fintype β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [StandardBorelSpace β₁] [Fintype β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] [StandardBorelSpace β₂] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (hln : IsBCLessNoisy W) {ν : MeasureTheory.Measure (ℕ × ℕ × α × β₁ × β₂)} [MeasureTheory.IsProbabilityMeasure ν] (h : IsUVChannelLaw W ν) {p : ℝ × ℝ} (hp : p ∈ uvRegion ν) :

p ∈ bcSuperpositionRegionNoSumRate W

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.bc_lessNoisy_uv_subset_superposition

source

bcOuterRegionUV W ⊆ bcSuperpositionRegionNoSumRate W

The UV outer region of a less noisy broadcast channel is contained in the two-constraint superposition inner bound over the full-support achievability pairs. The channel needs no support hypothesis here: the inclusion compares two single-letter regions, and positive mass on every output pair is asked for only where the inner bound is turned into codes (bcSuperpositionRegionNoSumRate_subset_capacity).

Used by

The capacity region of a less noisy channel #

theorem

InformationTheory.Shannon.BroadcastChannel.bc_lessNoisy_capacity_eq_uv

source

{α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [StandardBorelSpace α] [Fintype β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [StandardBorelSpace β₁] [Fintype β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] [StandardBorelSpace β₂] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (hW : ∀ (a : α) (b : β₁ × β₂), 0 < (W a).real {b}) (hln : IsBCLessNoisy W) :

bcCapacityRegion W = bcOuterRegionUV W

The capacity region of a less noisy broadcast channel whose transition law gives every output pair positive mass is its UV outer region bcOuterRegionUV, a single-letter expression in the four information slots of a five-tuple law.

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.bc_lessNoisy_superposition_eq_capacity

source

{α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [StandardBorelSpace α] [Fintype β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [StandardBorelSpace β₁] [Fintype β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] [StandardBorelSpace β₂] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (hW : ∀ (a : α) (b : β₁ × β₂), 0 < (W a).real {b}) (hln : IsBCLessNoisy W) :

bcSuperpositionRegionNoSumRate W = bcCapacityRegion W

Used by