InformationTheory.Shannon.ChannelCoding.ShannonTheorem

source

Imports 9

Shannon noisy channel coding theorem — full form (Cover-Thomas) #

Integrates input distribution maximization, expurgation (average → max error), and the main achievability argument.

Main definitions #

pmfToMeasure — lifts a pmf vector p : α → ℝ to a Measure α.
capacity — channel capacity sup { I(p; W).toReal | p ∈ stdSimplex }.
Code.subcode — restricts a code to a sub-message set.
pSmooth — smoothed input (1-δ) • p₀ + δ • uniform.
Code_lift_from_subtype — lifts a code on the support subtype to the full alphabet.

Main statements #

capacity_nonneg — capacity W ≥ 0.
exists_capacity_achiever — capacity is attained by some p ∈ stdSimplex.
capacity_lt_implies_exists_pmf — R < capacity W implies some p with R < I(p; W).
continuous_mutualInfoOfChannel_left — p ↦ I(pmfToMeasure p; W).toReal is continuous on stdSimplex.
channel_coding_achievability_max_error — average error → max error via expurgation.
mutualInfoOfChannel_restrict_to_support — MI is invariant under restriction to support.
shannon_noisy_channel_coding_theorem — for any R < capacity W and ε > 0, there exists N such that for all n ≥ N, a code of size ≥ exp(n R) with max error < ε.

References #

T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

Input distribution maximization #

noncomputable def

InformationTheory.Shannon.ChannelCoding.pmfToMeasure

source

{α : Type u_1} [Fintype α] [MeasurableSpace α] (p : α → ℝ) :

MeasureTheory.Measure α

Lift a pmf vector to a measure: pmfToMeasure p = ∑ a, ENNReal.ofReal (p a) • Measure.dirac a.

Equations

InformationTheory.Shannon.ChannelCoding.pmfToMeasure p = ∑ a : α, ENNReal.ofReal (p a) • MeasureTheory.Measure.dirac a

Instances For

Used by

theorem

InformationTheory.Shannon.ChannelCoding.pmfToMeasure_apply_singleton

source

{α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (p : α → ℝ) (a : α) :

(pmfToMeasure p) {a} = ENNReal.ofReal (p a)

Atom evaluation: (pmfToMeasure p) {a} = ENNReal.ofReal (p a).

Used by

theorem

InformationTheory.Shannon.ChannelCoding.pmfToMeasure_isProbabilityMeasure

source

{α : Type u_1} [Fintype α] [MeasurableSpace α] {p : α → ℝ} (hp : p ∈ stdSimplex ℝ α) :

MeasureTheory.IsProbabilityMeasure (pmfToMeasure p)

pmfToMeasure p is a probability measure when p ∈ stdSimplex ℝ α.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.pmfToMeasure_real_singleton

source

{α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {p : α → ℝ} (hp : p ∈ stdSimplex ℝ α) (a : α) :

(pmfToMeasure p).real {a} = p a

(pmfToMeasure p).real {a} = p a when p ∈ stdSimplex.

Used by

noncomputable def

InformationTheory.Shannon.ChannelCoding.capacity

source

{α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSpace β] (W : Channel α β) :

ℝ

Channel capacity capacity W := sup { I(p; W).toReal | p ∈ stdSimplex }.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.ChannelCoding.capacity_image_nonempty

source

{α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSpace β] (W : Channel α β) :

((fun (p : α → ℝ) => (mutualInfoOfChannel (pmfToMeasure p) W).toReal) '' stdSimplex ℝ α).Nonempty

The capacity image set is nonempty (witnessed by a Pi.single Dirac input).

Used by

theorem

InformationTheory.Shannon.ChannelCoding.capacity_bddAbove

source

BddAbove ((fun (p : α → ℝ) => (mutualInfoOfChannel (pmfToMeasure p) W).toReal) '' stdSimplex ℝ α)

capacity value set is bounded above by H(X) + H(Y)-style entropy bound.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.capacity_nonneg

source

0 ≤ capacity W

capacity W ≥ 0.

Used by

Continuity of `I(p; W).toReal` in p #

theorem

InformationTheory.Shannon.ChannelCoding.outputDistribution_real_singleton_of_stdSimplex

source

{α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace β] [MeasurableSingletonClass β] {p : α → ℝ} (hp : p ∈ stdSimplex ℝ α) (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (b : β) :

(outputDistribution (pmfToMeasure p) W).real {b} = ∑ a : α, p a * (W a).real {b}

For p ∈ stdSimplex, the output marginal (p ⊗ₘ W).snd real-value on {b} is ∑ a, p a · (W a).real {b}.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.mutualInfoOfChannel_toReal_eq_of_stdSimplex

source

(mutualInfoOfChannel (pmfToMeasure p) W).toReal = ∑ a : α, (p a).negMulLog + ∑ b : β, (∑ a : α, p a * (W a).real {b}).negMulLog - ∑ ab : α × β, (p ab.1 * (W ab.1).real {ab.2}).negMulLog

For p ∈ stdSimplex, I(pmfToMeasure p; W).toReal equals the 3-entropy expression in p.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.continuous_mutualInfoOfChannel_left

source

ContinuousOn (fun (p : α → ℝ) => (mutualInfoOfChannel (pmfToMeasure p) W).toReal) (stdSimplex ℝ α)

p ↦ (mutualInfoOfChannel (pmfToMeasure p) W).toReal is continuous on stdSimplex ℝ α.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.exists_capacity_achiever

source

∃ p ∈ stdSimplex ℝ α, IsMaxOn (fun (p : α → ℝ) => (mutualInfoOfChannel (pmfToMeasure p) W).toReal) (stdSimplex ℝ α) p

Capacity is attained: there exists p ∈ stdSimplex maximizing I(pmfToMeasure p; W).

Used by

theorem

InformationTheory.Shannon.ChannelCoding.capacity_lt_implies_exists_pmf

source

∃ p ∈ stdSimplex ℝ α, R < (mutualInfoOfChannel (pmfToMeasure p) W).toReal

R < capacity W implies there exists p ∈ stdSimplex with R < I(pmfToMeasure p; W).toReal.

Used by

Expurgation (average → max error) #

theorem

InformationTheory.Shannon.ChannelCoding.errorProbAt_filter_card_bound

source

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {M n : ℕ} (c : Code M n α β) (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] {K : ℝ} (hK : 1 < K) :

↑{m : Fin M | K * (c.averageErrorProb W).toReal < (c.errorProbAt W m).toReal}.card * K ≤ ↑M

Markov inequality: the number of m with errorProbAt > K · avg is at most M / K.

Used by

noncomputable def

InformationTheory.Shannon.ChannelCoding.Code.subcode

source

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {M n : ℕ} (c : Code M n α β) (S : Finset (Fin M)) (hS : 0 < S.card) :

Code S.card n α β

Sub-code restricted to a message subset S: encoder restricts to S, decoder maps outside S to a fixed fallback message.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.ChannelCoding.Code.subcode_errorProbAt_le

source

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {M n : ℕ} (c : Code M n α β) (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (S : Finset (Fin M)) (hS : 0 < S.card) (m' : Fin S.card) :

(c.subcode S hS).errorProbAt W m' ≤ c.errorProbAt W ↑(S.equivFin.symm ⟨↑m', ⋯⟩)

Sub-code error probability is bounded above by the original code's errorProbAt.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.tendsto_nat_mul_atTop

source

{c : ℝ} (hc : 0 < c) :

Filter.Tendsto (fun (n : ℕ) => ↑n * c) Filter.atTop Filter.atTop

Helper: linearization (fun n : ℕ => (n : ℝ) * c) → ∞ for c > 0.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.exists_N_two_ceil_exp_le

source

{R R' : ℝ} (hR_pos : 0 < R) (hRR' : R < R') :

∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → 2 * ⌈Real.exp (↑n * R)⌉₊ ≤ ⌈Real.exp (↑n * R')⌉₊

Helper: for 0 < R < R', eventually 2 * ⌈exp(n R)⌉ ≤ ⌈exp(n R')⌉.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.exists_subcode_maxError_lt_two_mul

source

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {n M' : ℕ} (c : Code M' n α β) (W' : Channel α β) [ProbabilityTheory.IsMarkovKernel W'] {R R' ε' : ℝ} (hR_pos : 0 < R) (hM'_lb : ⌈Real.exp (↑n * R')⌉₊ ≤ M') (hrate : 2 * ⌈Real.exp (↑n * R)⌉₊ ≤ ⌈Real.exp (↑n * R')⌉₊) (h_avg_lt : (c.averageErrorProb W').toReal < ε') :

∃ (M : ℕ) (_ : ⌈Real.exp (↑n * R)⌉₊ ≤ M) (cs : Code M n α β), ∀ (m : Fin M), (cs.errorProbAt W' m).toReal < 2 * ε'

Used by

theorem

InformationTheory.Shannon.ChannelCoding.channel_coding_achievability_max_error

source

{α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (hp_pos : ∀ (a : α), 0 < p.real {a}) (hW_pos : ∀ (a : α) (b : β), 0 < (W a).real {b}) {R : ℝ} (hR_pos : 0 < R) (hR : R < (mutualInfoOfChannel p W).toReal) {ε : ℝ} (hε : 0 < ε) :

∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ (M : ℕ) (_ : ⌈Real.exp (↑n * R)⌉₊ ≤ M) (c : Code M n α β), ∀ (m : Fin M), (c.errorProbAt W m).toReal < ε

Expurgation: average error achievability implies max error achievability.

Used by

Full-support assumption removal #

MI is invariant under restriction to the support {a | 0 < p.real {a}} via klDiv invariance under MeasurableEmbedding-pushforward.

theorem

InformationTheory.Shannon.ChannelCoding.mutualInfoOfChannel_restrict_to_support

source

{α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSpace β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] :

mutualInfoOfChannel p W = mutualInfoOfChannel (MeasureTheory.Measure.comap Subtype.val p) (ProbabilityTheory.Kernel.comap W Subtype.val ⋯)

Used by

noncomputable def

InformationTheory.Shannon.ChannelCoding.Code_lift_from_subtype

source

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {M n : ℕ} (p : MeasureTheory.Measure α) (c : Code M n { a : α // 0 < p.real {a} } β) :

Code M n α β

Lift a code from the support subtype to the full alphabet by composing the encoder with Subtype.val.

Equations

InformationTheory.Shannon.ChannelCoding.Code_lift_from_subtype p c = { encoder := fun (m : Fin M) (i : Fin n) => ↑(c.encoder m i), decoder := c.decoder }

Instances For

Used by

Main theorem #

noncomputable def

InformationTheory.Shannon.ChannelCoding.uniformInput

source

(α : Type u_3) [Fintype α] :

α → ℝ

Uniform input distribution unif a := 1/|α|, used as a smoothing target.

Equations

InformationTheory.Shannon.ChannelCoding.uniformInput α x✝ = (↑(Fintype.card α))⁻¹

Instances For

Used by

theorem

InformationTheory.Shannon.ChannelCoding.uniformInput_mem_stdSimplex

source

{α : Type u_1} [Fintype α] [Nonempty α] :

uniformInput α ∈ stdSimplex ℝ α

uniformInput α ∈ stdSimplex ℝ α.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.uniformInput_pos

source

{α : Type u_1} [Fintype α] [Nonempty α] (a : α) :

0 < uniformInput α a

uniformInput α a > 0 for any a.

Used by

noncomputable def

InformationTheory.Shannon.ChannelCoding.pSmooth

source

{α : Type u_1} [Fintype α] (p₀ : α → ℝ) (δ : ℝ) :

α → ℝ

Smoothed input pSmooth p₀ δ := (1-δ) • p₀ + δ • uniformInput.

Equations

InformationTheory.Shannon.ChannelCoding.pSmooth p₀ δ a = (1 - δ) * p₀ a + δ * InformationTheory.Shannon.ChannelCoding.uniformInput α a

Instances For

Used by

theorem

InformationTheory.Shannon.ChannelCoding.pSmooth_zero

source

{α : Type u_1} [Fintype α] (p₀ : α → ℝ) :

pSmooth p₀ 0 = p₀

pSmooth p₀ 0 = p₀.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.pSmooth_mem_stdSimplex

source

{α : Type u_1} [Fintype α] [Nonempty α] {p₀ : α → ℝ} (hp₀ : p₀ ∈ stdSimplex ℝ α) {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) :

pSmooth p₀ δ ∈ stdSimplex ℝ α

For δ ∈ [0,1] and p₀ ∈ stdSimplex, pSmooth p₀ δ ∈ stdSimplex.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.pSmooth_pos

source

{α : Type u_1} [Fintype α] [Nonempty α] {p₀ : α → ℝ} (hp₀ : p₀ ∈ stdSimplex ℝ α) {δ : ℝ} (hδ_pos : 0 < δ) (hδ1 : δ ≤ 1) (a : α) :

0 < pSmooth p₀ δ a

For δ ∈ (0,1] and p₀ ∈ stdSimplex, each entry (pSmooth p₀ δ) a > 0.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.continuous_pSmooth

source

{α : Type u_1} [Fintype α] (p₀ : α → ℝ) :

Continuous fun (δ : ℝ) => pSmooth p₀ δ

δ ↦ pSmooth p₀ δ is continuous (as a curve into α → ℝ with product topology).

Used by

theorem

InformationTheory.Shannon.ChannelCoding.shannon_noisy_channel_coding_theorem

source

{α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (hW_pos : ∀ (a : α) (b : β), 0 < (W a).real {b}) {R : ℝ} (hR_pos : 0 < R) (hR : R < capacity W) {ε : ℝ} (hε : 0 < ε) :

∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ (M : ℕ) (_ : ⌈Real.exp (↑n * R)⌉₊ ≤ M) (c : Code M n α β), ∀ (m : Fin M), (c.errorProbAt W m).toReal < ε

Shannon's noisy channel coding theorem: for any R < capacity W and ε > 0, there exists N such that for all n ≥ N there is a code of size ≥ exp(n R) achieving max error probability < ε.

Used by

InformationTheory.Shannon.ChannelCoding.ShannonTheorem

Shannon noisy channel coding theorem — full form (Cover-Thomas) #

Main definitions #

Main statements #

References #

Input distribution maximization #

Continuity of I(p; W).toReal in p #

Expurgation (average → max error) #

Full-support assumption removal #

Main theorem #

Continuity of `I(p; W).toReal` in p #