InformationTheory.Shannon.BroadcastChannel.Classes

Imports 3

Broadcast channel — comparison classes of the two receivers #

Three classes of two-receiver broadcast channel on which the first receiver is at least as good as the second. Two of them form a chain refining physical degradedness: a degraded channel is less noisy, and a less noisy channel is more capable. Semi-determinism is a separate condition on the first output alone and does not enter that chain.

Main definitions #

IsBCLessNoisy W — every auxiliary variable feeding the input carries at least as much information about the first output as about the second.
IsBCMoreCapable W — every input law reaches the first receiver at a rate at least that of the second.
IsBCSemiDeterministic W — the first output is a function of the input letter.

Main statements #

IsBCDegraded.isBCLessNoisy — a physically degraded channel is less noisy.
IsBCLessNoisy.isBCMoreCapable — a less noisy channel is more capable.
bc_lessNoisy_infoJoint_ge — over a less noisy channel the joint information I((U, X); Y₁) dominates the sum I(X; Y₁ ∣ U) + I(U; Y₂) of the two per-receiver informations.
IsBCSemiDeterministic.exists_prob_real_singleton_eq_zero_of_one_lt_card — a semi-deterministic channel with at least two first-output letters gives some output pair probability zero.

Implementation notes #

The auxiliary variable of IsBCLessNoisy ranges over the universe of the input alphabet, which is what lets the input itself be taken as the auxiliary; that instantiation is the whole step from less noisy to more capable.

The three classes #

def

InformationTheory.Shannon.BroadcastChannel.IsBCLessNoisy

source

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

Prop

The first receiver is less noisy than the second: for every auxiliary variable U feeding the input letter through a Markov kernel, the first output carries at least as much information about U as the second does. Unlike IsBCDegraded, this is a condition on the two output marginals of W only, not on their joint law.

Quantifying the auxiliary alphabet over the input alphabet's universe is no restriction: every finite type is measurably isomorphic to one of this universe, and mutual information is invariant under such a relabeling. @audit:ok

Equations

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

Instances For

Used by

def

InformationTheory.Shannon.BroadcastChannel.IsBCMoreCapable

source

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

Prop

The first receiver is more capable than the second: under every input law the first output carries at least as much information about the input as the second does. Stated on the two marginal channels Kernel.fst W and Kernel.snd W so that the channel-side vocabulary of mutualInfoOfChannel applies directly. @audit:ok

Equations

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

Instances For

Used by

def

InformationTheory.Shannon.BroadcastChannel.IsBCSemiDeterministic

source

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

Prop

The channel is semi-deterministic: the first output is a function of the input letter, while the second output stays arbitrary. Stated as an equality of the first marginal channel with a Dirac kernel, matching the ∃ kernel, ∀ letter, equality shape of IsBCDegraded. @audit:ok

Equations

InformationTheory.Shannon.BroadcastChannel.IsBCSemiDeterministic W = ∃ (f : α → β₁), ∀ (a : α), (ProbabilityTheory.Kernel.fst W) a = MeasureTheory.Measure.dirac (f a)

Instances For

Used by

Less noisy: the superposition rate sum #

theorem

InformationTheory.Shannon.BroadcastChannel.bc_lessNoisy_infoJoint_ge

source

{α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [DecidableEq β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [DecidableEq β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] {U : Type u} [Fintype U] [DecidableEq U] [Nonempty U] [MeasurableSpace U] [MeasurableSingletonClass U] (pU : MeasureTheory.Measure U) [MeasureTheory.IsProbabilityMeasure pU] (K : ProbabilityTheory.Kernel U α) [ProbabilityTheory.IsMarkovKernel K] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (hln : IsBCLessNoisy W) :

bcInfo₁ pU K W + bcInfo₂ pU K W ≤ bcInfoJoint pU K W

Superadditivity over a less noisy channel: the joint information I((U, X); Y₁) dominates the sum of the two per-receiver informations I(X; Y₁ ∣ U) + I(U; Y₂). Chain rule I((U, X); Y₁) = I(U; Y₁) + I(X; Y₁ ∣ U) plus the defining inequality I(U; Y₁) ≥ I(U; Y₂). This generalizes bc_degraded_infoJoint_ge, whose degradedness hypothesis is used only through that inequality. @audit:ok

Used by

Degraded implies less noisy #

theorem

InformationTheory.Shannon.BroadcastChannel.IsBCDegraded.isBCLessNoisy

source

IsBCLessNoisy W

A physically degraded channel is less noisy. Degradedness gives the Markov chain (U, X) → Y₁ → Y₂ on the per-coordinate joint law for every auxiliary; post-processing the source to U and applying data processing along the reversed chain yields the defining inequality. The reverse implication is not available: less noisy constrains only the two output marginals, degradedness their joint law. @audit:ok

Used by

Less noisy implies more capable #

theorem

InformationTheory.Shannon.BroadcastChannel.IsBCLessNoisy.isBCMoreCapable

source

IsBCMoreCapable W

A less noisy channel is more capable: take the input itself as the auxiliary variable, so that the defining inequality of IsBCLessNoisy at the identity kernel is the comparison of the two marginal channels. The reverse implication is not available: more capable compares the input alone, less noisy every auxiliary. @audit:ok

Used by

Semi-determinism and full support #

theorem

InformationTheory.Shannon.BroadcastChannel.IsBCSemiDeterministic.exists_prob_real_singleton_eq_zero_of_one_lt_card

source

∃ (b : β₁ × β₂), (W a).real {b} = 0

A semi-deterministic channel with at least two letters at the first output puts zero mass on some output pair: the first output is concentrated on f a, so every pair whose first component differs from f a is null. The full-support hypothesis of marton_achievability therefore fails on this class, so marton_region_subset_capacity is unavailable on it. @audit:ok

Used by