InformationTheory.Shannon.ChannelCoding.Achievability.Core

Imports 7

Channel coding achievability — core definitions #

Part of the longFile split of Achievability.lean. This part holds the i.i.d. input × channel plumbing, the codebook + joint-typical decoder, the per-codeword error decomposition, and the random codebook measure. The Fubini swap helpers and the random-codebook average bound live in ...Achievability.RandomCodebook; the pigeonhole and main theorem live in ...Achievability.Main.

i.i.d. input × channel plumbing #

noncomputable def

InformationTheory.Shannon.ChannelCoding.iidJointMeasure

source

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (p : MeasureTheory.Measure α) (W : Channel α β) (n : ℕ) :

MeasureTheory.Measure (Fin n → α × β)

The i.i.d. extension of (p, W) to length-n blocks: a measure on Fin n → α × β whose i-th coordinate has law jointDistribution p W.

Equations

InformationTheory.Shannon.ChannelCoding.iidJointMeasure p W n = MeasureTheory.Measure.pi fun (x : Fin n) => InformationTheory.Shannon.ChannelCoding.jointDistribution p W

Instances For

Used by

instance

InformationTheory.Shannon.ChannelCoding.iidJointMeasure.instIsProbabilityMeasure

source

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

MeasureTheory.IsProbabilityMeasure (iidJointMeasure p W n)

Used by

Codebook + joint-typical decoder #

abbrev

InformationTheory.Shannon.ChannelCoding.Codebook

source

@[reducible, inline]

(M n : ℕ) (α : Type u_3) [MeasurableSpace α] :

Type u_3

A random codebook is just a function from message indices to length-n words.

Equations

InformationTheory.Shannon.ChannelCoding.Codebook M n α = (Fin M → Fin n → α)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.ChannelCoding.jointTypicalDecoder

source

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Fintype β] {Ω : Type u_3} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) {M n : ℕ} (hM : 0 < M) (ε : ℝ) (codebook : Codebook M n α) :

(Fin n → β) → Fin M

Joint-typical decoder. Given a received word y, returns the unique message m such that (codebook m, y) ∈ jointlyTypicalSet μ Xs Ys n ε, falling back to ⟨0, hM⟩ if either no such m exists or it is not unique.

Equations

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

Instances For

Used by

noncomputable def

InformationTheory.Shannon.ChannelCoding.codebookToCode

source

Code M n α β

Bundle a codebook + joint-typical decoder into a Code.

Equations

InformationTheory.Shannon.ChannelCoding.codebookToCode μ Xs Ys hM ε codebook = { encoder := codebook, decoder := InformationTheory.Shannon.ChannelCoding.jointTypicalDecoder μ Xs Ys hM ε codebook }

Instances For

Used by

Per-codeword error decomposition #

theorem

InformationTheory.Shannon.ChannelCoding.errorProbAt_le_E1_plus_E2

source

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Fintype β] [MeasurableSingletonClass β] {Ω : Type u_3} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] {M n : ℕ} (hM : 0 < M) {ε : ℝ} (codebook : Codebook M n α) (m : Fin M) :

((codebookToCode μ Xs Ys hM ε codebook).errorProbAt W m).toReal ≤ (MeasureTheory.Measure.pi fun (i : Fin n) => W (codebook m i)).real {y : Fin n → β | (codebook m, y) ∉ jointlyTypicalSet μ Xs Ys n ε} + ∑ m' ∈ Finset.univ.erase m, (MeasureTheory.Measure.pi fun (i : Fin n) => W (codebook m i)).real {y : Fin n → β | (codebook m', y) ∈ jointlyTypicalSet μ Xs Ys n ε}

Per-codeword error bound. The point-wise error probability of message m under the joint-typical decoder is bounded by the (E1) "true codeword not typical" event plus the (E2) "some alias codeword is typical" union bound.

Used by

Random codebook average bound (probabilistic-method form) #

The random codebook is drawn from the standard Cover-Thomas product law p^{Mn} on Codebook M n α := Fin M → (Fin n → α): average over each codeword being p-i.i.d. on the input alphabet. The codebook law is codebookMeasure p M n := Measure.pi (fun _ : Fin M => Measure.pi (fun _ : Fin n => p)). Because α is finite, this Measure.pi is determined by its values on singletons {codebook}, namely the product ∏ m i, p.real {codebook m i}; the codebook average is then a finite weighted sum.

The alternative of averaging over a uniform distribution on Codebook M n α is inconsistent with the joint-typicality bounds, which speak about a p-i.i.d. law: when p is not uniform on α, the uniform-on-codebook expectation does not equal any p-derived quantity.

noncomputable def

InformationTheory.Shannon.ChannelCoding.codebookMeasure

source

{α : Type u_1} [MeasurableSpace α] (p : MeasureTheory.Measure α) (M n : ℕ) :

MeasureTheory.Measure (Codebook M n α)

Product law p^{Mn} on the codebook space.

Equations

InformationTheory.Shannon.ChannelCoding.codebookMeasure p M n = MeasureTheory.Measure.pi fun (x : Fin M) => MeasureTheory.Measure.pi fun (x : Fin n) => p

Instances For

Used by

instance

InformationTheory.Shannon.ChannelCoding.codebookMeasure.instIsProbabilityMeasure

source

{α : Type u_1} [MeasurableSpace α] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (M n : ℕ) :

MeasureTheory.IsProbabilityMeasure (codebookMeasure p M n)

Used by