InformationTheory.Shannon.BroadcastChannel.OuterBoundUV.Assembly
Broadcast channel — the operational capacity region lies in the UV outer region #
The UV outer region bcOuterRegionUV is the closure of a union of quadrilaterals indexed by the
five-tuple laws that the channel generates, the laws satisfying IsUVChannelLaw. What is left
is to exhibit a code as such a law: the letter laws of a code are channel laws, and time-sharing
mixes them into a single one whose information slots dominate the letter averages.
The main result is bc_capacity_subset_uv: the operational capacity region of the channel lies
in this region. The rate pair of a code, each coordinate discounted by the error probability of
its receiver and by two bits per letter, is a point of the quadrilateral of the time-shared letter
law; the discount vanishes as the error tolerance shrinks and the block length grows, and the
region is a closed lower set, so the limit and the rate pairs below it are in the region too.
Main definitions #
uvRelabel— re-encoding of the two auxiliary alphabets of a five-tuple.bcUVLetterKernel,bcUVLetterIndexLaw,bcUVTimeShare— the letter laws of a code read as a Markov kernel from the letter index, the uniform law of that index, and the resulting mixture.
Main statements #
bcUVJointDistribution_isUVChannelLaw— the letter-ilaw of a broadcast code is a channel law, so the letter laws of a code index the union.bcUVTimeShare_uvInfo₁_geand its three companions — each information slot of the time-shared law dominates the average of the letter slots.bc_uv_rate_sub_fanoSlack_mem_of_ceil_exp_le— the rate pair of a code, shrunk by the Fano slack per letter, lies in the region.bc_uv_logCard_mul_one_sub_errorProb_mem— the same in the form the asymptotic argument consumes: each rate is discounted by the error probability of its receiver and by two bits per letter, which no longer refers to the message count of the other receiver.bc_achievable_clamp_iff— clamping a rate pair into the first quadrant leaves achievability unchanged, since both ceilings equal one at a nonpositive rate.bc_uv_quadrant_mem_of_achievable— an achievable rate pair with nonnegative coordinates lies in the region, obtained from the code points by letting the error tolerance and the per-letter residue vanish.bc_capacity_subset_uv— the operational capacity region lies in the UV outer region.
Implementation notes #
The asymptotic argument runs on bc_uv_logCard_mul_one_sub_errorProb_mem rather than on
bc_uv_rate_sub_fanoSlack_mem_of_ceil_exp_le: the latter subtracts the sum of both Fano slacks
from each coordinate, and a slack of the other receiver is not controlled by the rate of this
one, since the message counts of an achievable pair are bounded from below only. Discounting
each rate by its own error probability removes that coupling, and the residue is two bits per
block whatever the message counts are.
The letter laws of a code are channel laws #
InformationTheory.Shannon.BroadcastChannel.bcUVJointDistribution_isUVChannelLaw
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{M₁ M₂ n : ℕ}
[Nonempty β₁]
[Nonempty β₂]
(c : BroadcastCode M₁ M₂ n α β₁ β₂)
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
[NeZero M₁]
[NeZero M₂]
(i : Fin n)
:
IsUVChannelLaw W (bcUVJointDistribution c W i)
@audit:ok
Used by
Re-encoding the auxiliary alphabets #
InformationTheory.Shannon.BroadcastChannel.uvRelabel
source{α : Type u_1}
{β₁ : Type u_2}
{β₂ : Type u_3}
{U : Type u_4}
{V : Type u_5}
{U' : Type u_6}
{V' : Type u_7}
(e₁ : U → U')
(e₂ : V → V')
:
Re-encoding of the two auxiliary alphabets of a five-tuple, leaving the input letter and the two output letters alone.
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.measurable_uvRelabel
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
{V : Type u_5}
{U' : Type u_6}
{V' : Type u_7}
[MeasurableSpace U]
[MeasurableSpace V]
[MeasurableSpace U']
[MeasurableSpace V']
{e₁ : U → U'}
{e₂ : V → V'}
(he₁ : Measurable e₁)
(he₂ : Measurable e₂)
:
Measurable (uvRelabel e₁ e₂)
Used by
InformationTheory.Shannon.BroadcastChannel.uvInfo₁_map_uvRelabel
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
{V : Type u_5}
{U' : Type u_6}
{V' : Type u_7}
[MeasurableSpace U]
[MeasurableSpace V]
[MeasurableSpace U']
[MeasurableSpace V']
(ν : MeasureTheory.Measure (U × V × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
{e₁ : U → U'}
{e₂ : V → V'}
{d₂ : V' → V}
(he₁ : Measurable e₁)
(he₂ : Measurable e₂)
(hd₂ : Measurable d₂)
(h₂ : ∀ (v : V), d₂ (e₂ v) = v)
:
Used by
InformationTheory.Shannon.BroadcastChannel.uvInfo₂_map_uvRelabel
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
{V : Type u_5}
{U' : Type u_6}
{V' : Type u_7}
[MeasurableSpace U]
[MeasurableSpace V]
[MeasurableSpace U']
[MeasurableSpace V']
(ν : MeasureTheory.Measure (U × V × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
{e₁ : U → U'}
{e₂ : V → V'}
{d₁ : U' → U}
(he₁ : Measurable e₁)
(he₂ : Measurable e₂)
(hd₁ : Measurable d₁)
(h₁ : ∀ (u : U), d₁ (e₁ u) = u)
:
Used by
InformationTheory.Shannon.BroadcastChannel.uvInfoJoint_map_uvRelabel
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
{V : Type u_5}
{U' : Type u_6}
{V' : Type u_7}
[MeasurableSpace U]
[MeasurableSpace V]
[MeasurableSpace U']
[MeasurableSpace V']
(ν : MeasureTheory.Measure (U × V × α × β₁ × β₂))
{e₁ : U → U'}
{e₂ : V → V'}
(he₁ : Measurable e₁)
(he₂ : Measurable e₂)
:
Used by
InformationTheory.Shannon.BroadcastChannel.uvInfoSum₂_map_uvRelabel
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
{V : Type u_5}
{U' : Type u_6}
{V' : Type u_7}
[MeasurableSpace U]
[MeasurableSpace V]
[MeasurableSpace U']
[MeasurableSpace V']
[StandardBorelSpace α]
[Nonempty α]
[Fintype β₁]
[MeasurableSingletonClass β₁]
[StandardBorelSpace β₁]
[Nonempty β₁]
[Fintype U]
[MeasurableSingletonClass U]
(ν : MeasureTheory.Measure (U × V × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
{e₁ : U → U'}
{e₂ : V → V'}
{d₁ : U' → U}
(he₁ : Measurable e₁)
(he₂ : Measurable e₂)
(hd₁ : Measurable d₁)
(h₁ : ∀ (u : U), d₁ (e₁ u) = u)
:
Used by
InformationTheory.Shannon.BroadcastChannel.uvInfoSum₁_map_uvRelabel
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{U : Type u_4}
{V : Type u_5}
{U' : Type u_6}
{V' : Type u_7}
[MeasurableSpace U]
[MeasurableSpace V]
[MeasurableSpace U']
[MeasurableSpace V']
[StandardBorelSpace α]
[Nonempty α]
[Fintype β₂]
[MeasurableSingletonClass β₂]
[StandardBorelSpace β₂]
[Nonempty β₂]
[Fintype V]
[MeasurableSingletonClass V]
(ν : MeasureTheory.Measure (U × V × α × β₁ × β₂))
[MeasureTheory.IsProbabilityMeasure ν]
{e₁ : U → U'}
{e₂ : V → V'}
{d₂ : V' → V}
(he₁ : Measurable e₁)
(he₂ : Measurable e₂)
(hd₂ : Measurable d₂)
(h₂ : ∀ (v : V), d₂ (e₂ v) = v)
:
Used by
Time sharing #
The time-shared five-tuple law #
InformationTheory.Shannon.BroadcastChannel.bcUVLetterKernel
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{M₁ M₂ n : ℕ}
[Nonempty β₁]
[Nonempty β₂]
(c : BroadcastCode M₁ M₂ n α β₁ β₂)
(W : BCChannel α β₁ β₂)
:
The letter laws of a broadcast code, read as a Markov kernel from the letter index.
Equations
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.bcUVLetterIndexLaw
sourceThe uniform law of the letter index of a length-n block code.
Equations
Instances For
Used by
InformationTheory.Shannon.BroadcastChannel.bcUVLetterIndexLaw_isProbabilityMeasure
sourceUsed by
InformationTheory.Shannon.BroadcastChannel.bcUVLetterKernel_apply
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{M₁ M₂ n : ℕ}
[Nonempty β₁]
[Nonempty β₂]
(c : BroadcastCode M₁ M₂ n α β₁ β₂)
(W : BCChannel α β₁ β₂)
(i : Fin n)
:
Used by
InformationTheory.Shannon.BroadcastChannel.bcUVLetterKernel_isMarkovKernel
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{M₁ M₂ n : ℕ}
[Nonempty β₁]
[Nonempty β₂]
(c : BroadcastCode M₁ M₂ n α β₁ β₂)
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
[NeZero M₁]
[NeZero M₂]
:
Used by
InformationTheory.Shannon.BroadcastChannel.bcUVLetterKernel_ae_tag
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{M₁ M₂ n : ℕ}
[Fintype α]
[MeasurableSingletonClass α]
[Fintype β₁]
[MeasurableSingletonClass β₁]
[Nonempty β₁]
[Fintype β₂]
[MeasurableSingletonClass β₂]
[Nonempty β₂]
(c : BroadcastCode M₁ M₂ n α β₁ β₂)
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
[NeZero M₁]
[NeZero M₂]
[NeZero n]
:
Used by
The four slots of the time-shared law dominate the letter averages #
InformationTheory.Shannon.BroadcastChannel.lintegral_bcUVLetterIndexLaw
sourceUsed by
The shrunk rate point #
InformationTheory.Shannon.BroadcastChannel.bc_uv_mem_of_mul_le_slot_sums
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{M₁ M₂ n : ℕ}
[Fintype α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
[Nonempty α]
[Fintype β₁]
[MeasurableSingletonClass β₁]
[StandardBorelSpace β₁]
[Nonempty β₁]
[Fintype β₂]
[MeasurableSingletonClass β₂]
[StandardBorelSpace β₂]
[Nonempty β₂]
[NeZero M₁]
[NeZero M₂]
(c : BroadcastCode M₁ M₂ n α β₁ β₂)
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(hn : 0 < n)
{r₁ r₂ : ℝ}
(hb₁ : ↑n * r₁ ≤ (∑ i : Fin n, uvInfo₁ (bcUVJointDistribution c W i)).toReal)
(hb₂ : ↑n * r₂ ≤ (∑ i : Fin n, uvInfo₂ (bcUVJointDistribution c W i)).toReal)
(hb₃ : ↑n * (r₁ + r₂) ≤ (∑ i : Fin n, uvInfoSum₂ (bcUVJointDistribution c W i)).toReal)
(hb₄ : ↑n * (r₁ + r₂) ≤ (∑ i : Fin n, uvInfoSum₁ (bcUVJointDistribution c W i)).toReal)
:
@audit:ok
Used by
InformationTheory.Shannon.BroadcastChannel.bcConverseFanoSlack₁_le
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{M₁ M₂ n : ℕ}
[Fintype β₁]
[MeasurableSingletonClass β₁]
[Fintype β₂]
[MeasurableSingletonClass β₂]
[NeZero M₁]
[NeZero M₂]
(c : BroadcastCode M₁ M₂ n α β₁ β₂)
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(hcard₁ : 2 ≤ M₁)
:
@audit:ok
Used by
InformationTheory.Shannon.BroadcastChannel.bcConverseFanoSlack₂_le
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{M₁ M₂ n : ℕ}
[Fintype β₁]
[MeasurableSingletonClass β₁]
[Fintype β₂]
[MeasurableSingletonClass β₂]
[NeZero M₁]
[NeZero M₂]
(c : BroadcastCode M₁ M₂ n α β₁ β₂)
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(hcard₂ : 2 ≤ M₂)
:
@audit:ok
Used by
InformationTheory.Shannon.BroadcastChannel.bc_uv_converse_slots
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{M₁ M₂ n : ℕ}
[Fintype α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
[Nonempty α]
[Fintype β₁]
[MeasurableSingletonClass β₁]
[StandardBorelSpace β₁]
[Nonempty β₁]
[Fintype β₂]
[MeasurableSingletonClass β₂]
[StandardBorelSpace β₂]
[Nonempty β₂]
[NeZero M₁]
[NeZero M₂]
(c : BroadcastCode M₁ M₂ n α β₁ β₂)
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(hcard₁ : 2 ≤ M₁)
(hcard₂ : 2 ≤ M₂)
:
InBCOuterRegionUV (Real.log ↑M₁) (Real.log ↑M₂)
((∑ i : Fin n, uvInfo₁ (bcUVJointDistribution c W i)).toReal + bcConverseFanoSlack₁ c W)
((∑ i : Fin n, uvInfo₂ (bcUVJointDistribution c W i)).toReal + bcConverseFanoSlack₂ c W)
((∑ i : Fin n, uvInfoSum₂ (bcUVJointDistribution c W i)).toReal + bcConverseFanoSlack₁ c W + bcConverseFanoSlack₂ c W)
((∑ i : Fin n, uvInfoSum₁ (bcUVJointDistribution c W i)).toReal + bcConverseFanoSlack₁ c W + bcConverseFanoSlack₂ c W)
@audit:ok
Used by
InformationTheory.Shannon.BroadcastChannel.bc_uv_rate_sub_fanoSlack_mem_of_ceil_exp_le
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{M₁ M₂ n : ℕ}
[Fintype α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
[Nonempty α]
[Fintype β₁]
[MeasurableSingletonClass β₁]
[StandardBorelSpace β₁]
[Nonempty β₁]
[Fintype β₂]
[MeasurableSingletonClass β₂]
[StandardBorelSpace β₂]
[Nonempty β₂]
[NeZero M₁]
[NeZero M₂]
(c : BroadcastCode M₁ M₂ n α β₁ β₂)
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(hn : 0 < n)
(hcard₁ : 2 ≤ M₁)
(hcard₂ : 2 ≤ M₂)
{R₁ R₂ : ℝ}
(hM₁ : ⌈Real.exp (↑n * R₁)⌉₊ ≤ M₁)
(hM₂ : ⌈Real.exp (↑n * R₂)⌉₊ ≤ M₂)
:
(R₁ - (bcConverseFanoSlack₁ c W + bcConverseFanoSlack₂ c W) / ↑n, R₂ - (bcConverseFanoSlack₁ c W + bcConverseFanoSlack₂ c W) / ↑n) ∈ bcOuterRegionUV W
The rate pair of a broadcast code, shrunk by the per-letter Fano slack, lies in the UV outer region. The letter index is absorbed into the auxiliaries, which already carry it, so the average of the letter laws is again a channel law and dominates the per-letter averages of all four information slots. @audit:ok
Used by
InformationTheory.Shannon.BroadcastChannel.bc_uv_logCard_mul_one_sub_errorProb_mem
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{M₁ M₂ n : ℕ}
[Fintype α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
[Nonempty α]
[Fintype β₁]
[MeasurableSingletonClass β₁]
[StandardBorelSpace β₁]
[Nonempty β₁]
[Fintype β₂]
[MeasurableSingletonClass β₂]
[StandardBorelSpace β₂]
[Nonempty β₂]
[NeZero M₁]
[NeZero M₂]
(c : BroadcastCode M₁ M₂ n α β₁ β₂)
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(hn : 0 < n)
(hcard₁ : 2 ≤ M₁)
(hcard₂ : 2 ≤ M₂)
:
The rate pair of a broadcast code, each coordinate discounted by the error probability of its
own receiver and by two bits per letter, lies in the UV outer region. Bounding a Fano slack by
log 2 + Pe * log M turns it into a discount on the rate of its own receiver, so neither
coordinate refers to the message count of the other one.
@audit:ok
Used by
InformationTheory.Shannon.BroadcastChannel.bc_uv_rate_mem_of_mul_le_logCard
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{M₁ M₂ n : ℕ}
[Fintype α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
[Nonempty α]
[Fintype β₁]
[MeasurableSingletonClass β₁]
[StandardBorelSpace β₁]
[Nonempty β₁]
[Fintype β₂]
[MeasurableSingletonClass β₂]
[StandardBorelSpace β₂]
[Nonempty β₂]
[NeZero M₁]
[NeZero M₂]
(c : BroadcastCode M₁ M₂ n α β₁ β₂)
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(hn : 0 < n)
(hcard₁ : 2 ≤ M₁)
(hcard₂ : 2 ≤ M₂)
{r₁ r₂ : ℝ}
(h₁ : ↑n * r₁ ≤ Real.log ↑M₁ * (1 - (c.averageErrorProb₁ W).toReal))
(h₂ : ↑n * r₂ ≤ Real.log ↑M₂ * (1 - (c.averageErrorProb₂ W).toReal))
:
@audit:ok
Used by
The operational region lies in the UV outer region #
InformationTheory.Shannon.BroadcastChannel.bc_achievable_clamp_iff
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
(W : BCChannel α β₁ β₂)
(R₁ R₂ : ℝ)
:
Clamping a rate pair into the first quadrant leaves achievability unchanged: at a nonpositive
rate the message count ⌈exp (n * R)⌉ a code is asked to carry is one, the same value it takes at
rate zero.
@audit:ok
Used by
InformationTheory.Shannon.BroadcastChannel.bc_uv_rate_mul_one_sub_mem_of_errorProb_le
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
{M₁ M₂ n : ℕ}
[Fintype α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
[Nonempty α]
[Fintype β₁]
[MeasurableSingletonClass β₁]
[StandardBorelSpace β₁]
[Nonempty β₁]
[Fintype β₂]
[MeasurableSingletonClass β₂]
[StandardBorelSpace β₂]
[Nonempty β₂]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
(c : BroadcastCode M₁ M₂ n α β₁ β₂)
(hn : 0 < n)
{R₁ R₂ ε : ℝ}
(hR₁ : 0 ≤ R₁)
(hR₂ : 0 ≤ R₂)
(hε1 : ε ≤ 1)
(hM₁ : ⌈Real.exp (↑n * R₁)⌉₊ ≤ M₁)
(hM₂ : ⌈Real.exp (↑n * R₂)⌉₊ ≤ M₂)
(he₁ : (c.averageErrorProb₁ W).toReal ≤ ε)
(he₂ : (c.averageErrorProb₂ W).toReal ≤ ε)
:
@audit:ok
Used by
InformationTheory.Shannon.BroadcastChannel.bc_uv_quadrant_mem_of_achievable
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
[Fintype α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
[Nonempty α]
[Fintype β₁]
[MeasurableSingletonClass β₁]
[StandardBorelSpace β₁]
[Nonempty β₁]
[Fintype β₂]
[MeasurableSingletonClass β₂]
[StandardBorelSpace β₂]
[Nonempty β₂]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
{R₁ R₂ : ℝ}
(hR₁ : 0 ≤ R₁)
(hR₂ : 0 ≤ R₂)
(hach : BCAchievable W R₁ R₂)
:
An achievable rate pair with nonnegative coordinates lies in the UV outer region. For every error tolerance and every block length the pair, discounted by the error probability of each receiver and by two bits per letter, is a point of the region; those points converge to the pair itself as the tolerance shrinks and the block length grows, and the region is closed. @audit:ok
Used by
InformationTheory.Shannon.BroadcastChannel.bc_capacity_subset_uv
source{α : Type u_1}
[MeasurableSpace α]
{β₁ : Type u_2}
[MeasurableSpace β₁]
{β₂ : Type u_3}
[MeasurableSpace β₂]
[Fintype α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
[Nonempty α]
[Fintype β₁]
[MeasurableSingletonClass β₁]
[StandardBorelSpace β₁]
[Nonempty β₁]
[Fintype β₂]
[MeasurableSingletonClass β₂]
[StandardBorelSpace β₂]
[Nonempty β₂]
(W : BCChannel α β₁ β₂)
[ProbabilityTheory.IsMarkovKernel W]
:
The operational capacity region of a broadcast channel is contained in the UV (Nair–El Gamal)
outer region. Together with marton_region_subset_capacity this places the capacity region
between Marton's inner bound and the UV outer bound as subsets of the plane.
Nonpositive rates are covered without a sign hypothesis: clamping a rate pair into the first quadrant leaves achievability unchanged, and the outer region is a lower set, so the clamped pair carries the original one. @audit:ok