InformationTheory.Shannon.AWGN.AchievabilityCodebook

Imports 10

The random Gaussian codebook #

The random codebook law for AWGN achievability (Cover–Thomas): M codewords, each with n i.i.d. 𝒩(0, σsq) components, carried by Fin M → Fin n → ℝ and built as a two-stage Measure.pi so that it is definitionally equal to AwgnCode.encoder.

Main definitions #

gaussianCodebook M n σsq — the random codebook law.

Main statements #

gaussianCodebook_codeword_law — projecting onto a single codeword index gives the inner i.i.d. Gaussian product measure.
gaussianCodebook_indepFun_codewords — distinct codewords are independent.

Random Gaussian codebook #

noncomputable def

InformationTheory.Shannon.AWGN.gaussianCodebook

source

(M n : ℕ) (σsq : NNReal) :

MeasureTheory.Measure (Fin M → Fin n → ℝ)

The random Gaussian codebook: M codewords, each n i.i.d. components X(m, i) ∼ 𝒩(0, σsq), built as a two-stage Measure.pi. The concrete carrier type Fin M → Fin n → ℝ matches AwgnCode.encoder definitionally, so no measurable-equivalence transport is needed.

Equations

InformationTheory.Shannon.AWGN.gaussianCodebook M n σsq = MeasureTheory.Measure.pi fun (x : Fin M) => MeasureTheory.Measure.pi fun (x : Fin n) => ProbabilityTheory.gaussianReal 0 σsq

Instances For

Used by

instance

InformationTheory.Shannon.AWGN.gaussianCodebook_isProbabilityMeasure

source

(M n : ℕ) (σsq : NNReal) :

MeasureTheory.IsProbabilityMeasure (gaussianCodebook M n σsq)

gaussianCodebook M n σsq is a probability measure (2-stage Measure.pi of the probability measure gaussianReal 0 σsq). All instances autoderive via pi.instIsProbabilityMeasure + instIsProbabilityMeasureGaussianReal.

Used by

theorem

InformationTheory.Shannon.AWGN.gaussianCodebook_codeword_law

source

(M n : ℕ) (σsq : NNReal) (m : Fin M) :

MeasureTheory.Measure.map (fun (c : Fin M → Fin n → ℝ) => c m) (gaussianCodebook M n σsq) = MeasureTheory.Measure.pi fun (x : Fin n) => ProbabilityTheory.gaussianReal 0 σsq

Projecting gaussianCodebook onto codeword index m gives back the inner i.i.d. Gaussian product measure on Fin n → ℝ.

Used by

theorem

InformationTheory.Shannon.AWGN.gaussianCodebook_indepFun_codewords

source

(M n : ℕ) (σsq : NNReal) {m m' : Fin M} (hmm' : m ≠ m') :

ProbabilityTheory.IndepFun (fun (c : Fin M → Fin n → ℝ) => c m) (fun (c : Fin M → Fin n → ℝ) => c m') (gaussianCodebook M n σsq)

Under the codebook law, distinct codewords c m, c m' are independent random variables.

Used by