InformationTheory.Shannon.ChannelCoding.ShannonTheoremGeneral

Imports 7

Shannon noisy channel coding theorem — smoothing infrastructure #

Smoothing infrastructure for the Shannon noisy channel coding theorem without the full-support assumption hW_pos. The smoothed channel is Channel.smooth W δ a := (1-δ) · W a + δ · uniformMeasureβ.

Main definitions #

uniformMeasureβ β: uniform probability measure on a finite type β.
Channel.smooth W δ: convex combination of W with the uniform output measure.

Main statements #

exists_smooth_capacity_gt: from R < capacity W, extracts δ_B > 0 and R₁ > R with R₁ < capacity (W_smooth δ) for all δ ∈ (0, δ_B].
errorProbAt_smooth_TV: TV bound |errorProbAt(W_smooth δ) - errorProbAt(W)| ≤ 2 n δ.

Implementation notes #

The main theorem shannon_noisy_channel_coding_theorem_general is in ShannonTheoremMaxError, which imports this file for the smoothing infrastructure.

Smoothed channel definition and basic properties #

noncomputable def

InformationTheory.Shannon.ChannelCoding.uniformMeasureβ

source

(β : Type u_3) [Fintype β] [MeasurableSpace β] :

MeasureTheory.Measure β

Uniform probability measure on a nonempty finite type β.

Equations

InformationTheory.Shannon.ChannelCoding.uniformMeasureβ β = (↑(Fintype.card β))⁻¹ • ∑ b : β, MeasureTheory.Measure.dirac b

Instances For

Used by

instance

InformationTheory.Shannon.ChannelCoding.uniformMeasureβ_isProbabilityMeasure

source

{β : Type u_2} [Fintype β] [Nonempty β] [MeasurableSpace β] :

MeasureTheory.IsProbabilityMeasure (uniformMeasureβ β)

uniformMeasureβ is a probability measure (since β is nonempty).

Used by

theorem

InformationTheory.Shannon.ChannelCoding.uniformMeasureβ_real_singleton

source

{β : Type u_2} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (b : β) :

(uniformMeasureβ β).real {b} = (↑(Fintype.card β))⁻¹

Atom evaluation: (uniformMeasureβ).real {b} = 1/|β|.

Used by

noncomputable def

InformationTheory.Shannon.ChannelCoding.Channel.smooth

source

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

Channel α β

Smoothed channel W_smooth δ a := (1-δ) W a + δ · uniformMeasureβ.

Equations

W.smooth δ = { toFun := fun (a : α) => ENNReal.ofReal (1 - δ) • W a + ENNReal.ofReal δ • InformationTheory.Shannon.ChannelCoding.uniformMeasureβ β, measurable' := ⋯ }

Instances For

Used by

theorem

InformationTheory.Shannon.ChannelCoding.Channel.smooth_apply

source

@[simp]

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

(W.smooth δ) a = ENNReal.ofReal (1 - δ) • W a + ENNReal.ofReal δ • uniformMeasureβ β

Used by

theorem

InformationTheory.Shannon.ChannelCoding.Channel.smooth_zero

source

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

W.smooth 0 = W

Channel.smooth W 0 = W.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.Channel.smooth_isMarkovKernel

source

{α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) :

ProbabilityTheory.IsMarkovKernel (W.smooth δ)

For δ ∈ [0,1], Channel.smooth W δ is a Markov kernel.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.Channel.smooth_real_singleton

source

{α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) (a : α) (b : β) :

((W.smooth δ) a).real {b} = (1 - δ) * (W a).real {b} + δ * (↑(Fintype.card β))⁻¹

For δ ∈ [0,1], (W_smooth δ a).real {b} = (1-δ)(W a).real{b} + δ/|β|.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.Channel.smooth_pos

source

{α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] {δ : ℝ} (hδ_pos : 0 < δ) (hδ1 : δ ≤ 1) (a : α) (b : β) :

0 < ((W.smooth δ) a).real {b}

For δ ∈ (0,1], every atom of W_smooth δ a has positive probability.

Used by

Mutual information continuity in `δ` #

theorem

InformationTheory.Shannon.ChannelCoding.mutualInfoOfChannel_toReal_three_entropy

source

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

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

Helper: for any Markov channel K, the 3-entropy form of MI in terms of (K a).real {b}.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.mutualInfoOfChannel_toReal_smooth_eq

source

{α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] {p : α → ℝ} (hp : p ∈ stdSimplex ℝ α) (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) :

(mutualInfoOfChannel (pmfToMeasure p) (W.smooth δ)).toReal = ∑ a : α, (p a).negMulLog + ∑ b : β, (∑ a : α, p a * ((1 - δ) * (W a).real {b} + δ * (↑(Fintype.card β))⁻¹)).negMulLog - ∑ ab : α × β, (p ab.1 * ((1 - δ) * (W ab.1).real {ab.2} + δ * (↑(Fintype.card β))⁻¹)).negMulLog

For δ ∈ [0,1], (mutualInfoOfChannel (pmfToMeasure p) (Channel.smooth W δ)).toReal expands in the 3-entropy form with (W_smooth δ a).real {b} substituted via smooth_real_singleton.

Used by

theorem

InformationTheory.Shannon.ChannelCoding.continuous_mutualInfoOfChannel_right_smooth

source

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

ContinuousOn (fun (δ : ℝ) => (mutualInfoOfChannel (pmfToMeasure p) (W.smooth δ)).toReal) (Set.Icc 0 1)

δ ↦ (mutualInfoOfChannel (pmfToMeasure p) (Channel.smooth W δ)).toReal is continuous on [0,1].

Used by

TV bound #

theorem

InformationTheory.Shannon.ChannelCoding.errorProbAt_smooth_TV

source

{α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] {M n : ℕ} (c : Code M n α β) (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] {δ : ℝ} (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) (m : Fin M) :

|(c.errorProbAt (W.smooth δ) m).toReal - (c.errorProbAt W m).toReal| ≤ 2 * ↑n * δ

For δ ∈ [0,1], the difference between errorProbAt under W and W_smooth δ is bounded by 2 n δ.

Used by

InformationTheory.Shannon.ChannelCoding.ShannonTheoremGeneral

Shannon noisy channel coding theorem — smoothing infrastructure #

Main definitions #

Main statements #

Implementation notes #

Smoothed channel definition and basic properties #

Mutual information continuity in δ #

TV bound #

TV bound #

Mutual information continuity in `δ` #