InformationTheory.Shannon.AWGN.AchievabilityCodeExistence

Imports 13

AWGN achievability assembly #

The assembled achievability statement for the AWGN channel coding theorem (Cover–Thomas): combining the random Gaussian codebook, the joint-typicality decoder and union bound, the power-constraint witness, and worst-half expurgation into the existence of good (M, n) codes for any rate below the Gaussian capacity.

Main statements #

isAwgnTypicalityHypothesis — the assembled achievability statement consumed by the headline awgn_achievability.

Achievability assembly #

theorem

InformationTheory.Shannon.AWGN.errorEvent_jointTypicalDecoder_comp_subset_of_strictMono

source

{n M M_target : ℕ} [NeZero M] [NeZero M_target] (A : Set ((Fin n → ℝ) × (Fin n → ℝ))) (c : Fin M → Fin n → ℝ) (reindex : Fin M_target → Fin M) (hreindex_strictMono : StrictMono reindex) (j : Fin M_target) :

{ encoder := fun (i : Fin M_target) => c (reindex i), decoder := jointTypicalDecoder A fun (i : Fin M_target) => c (reindex i) }.errorEvent j ⊆ { encoder := c, decoder := jointTypicalDecoder A c }.errorEvent (reindex j)

The assembled AWGN achievability statement: for any rate R below the Gaussian capacity and any ε > 0, there is a threshold N₀ such that for every n ≥ N₀ there is an (M, n) code (with M ≥ ⌈exp(nR)⌉) whose maximal per-message error probability over the AWGN channel is below ε.

The assembly combines a strictly smaller slack variance P' from awgnPowerWitness_exists, a typicality slack δ := (C−R)/12 for the union-bound margin R'' + 3δ < C, the typical set and its two AEP bounds from continuousAepGaussian_holds P' N, the per-message error bound from awgn_random_coding_union_bound P' N h_meas, and the power constraint from the per-codeword expurgation bound awgnPowerConstraintPerCodeword_holds P' P N.

The strict witness hP'_pos : 0 < P' (from awgnPowerWitness_exists) + hN are supplied to awgn_random_coding_union_bound. @audit:ok

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_errorEvent_aemeasurable

source

{n M : ℕ} [NeZero M] (P' : ℝ) (N : NNReal) (h_meas : IsAwgnChannelMeasurable N) (A : Set ((Fin n → ℝ) × (Fin n → ℝ))) (hA_meas : MeasurableSet A) (m : Fin M) :

AEMeasurable (fun (c : Fin M → Fin n → ℝ) => (MeasureTheory.Measure.pi fun (i : Fin n) => (awgnChannel N h_meas) (c m i)) ({ encoder := c, decoder := jointTypicalDecoder A c }.errorEvent m)) (gaussianCodebook M n P'.toNNReal)

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_subcodebook_errorEvent_le

source

{n M M_target : ℕ} [NeZero M] [NeZero M_target] (N : NNReal) (h_meas : IsAwgnChannelMeasurable N) (A : Set ((Fin n → ℝ) × (Fin n → ℝ))) (c_full : Fin M → Fin n → ℝ) (reindex : Fin M_target → Fin M) (hreindex_strictMono : StrictMono reindex) {b : ENNReal} (hfull : ∀ (j : Fin M_target), (MeasureTheory.Measure.pi fun (i : Fin n) => (awgnChannel N h_meas) (c_full (reindex j) i)) ({ encoder := c_full, decoder := jointTypicalDecoder A c_full }.errorEvent (reindex j)) ≤ b) (j : Fin M_target) :

(MeasureTheory.Measure.pi fun (i : Fin n) => (awgnChannel N h_meas) (c_full (reindex j) i)) ({ encoder := fun (i : Fin M_target) => c_full (reindex i), decoder := jointTypicalDecoder A fun (i : Fin M_target) => c_full (reindex i) }.errorEvent j) ≤ b

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_exists_codebook_combined_penalty

source

{n M : ℕ} [NeZero M] (P P' : ℝ) (N : NNReal) (h_meas : IsAwgnChannelMeasurable N) (A : Set ((Fin n → ℝ) × (Fin n → ℝ))) (hA_meas : MeasurableSet A) (hM_ge_two : 2 ≤ M) {ε_rand ε_pow ε_d2 : ℝ} (hε_rand_nonneg : 0 ≤ ε_rand) (hε_pow_pos : 0 < ε_pow) (hε_d2_pos : 0 < ε_d2) (h_slack_eq : 2 * ε_rand + ε_pow = 2 * ε_d2) (h4_lt_one : 4 * ε_d2 < 1) (h_per_m : ∀ (m : Fin M), ∫⁻ (c : Fin M → Fin n → ℝ), (MeasureTheory.Measure.pi fun (i : Fin n) => (awgnChannel N h_meas) (c m i)) ({ encoder := c, decoder := jointTypicalDecoder A c }.errorEvent m) ∂gaussianCodebook M n P'.toNNReal ≤ ENNReal.ofReal (2 * ε_rand)) (h_viol_mass : ∀ (m : Fin M), (gaussianCodebook M n P'.toNNReal) {c : Fin M → Fin n → ℝ | ↑n * P < ∑ i : Fin n, c m i ^ 2} ≤ ENNReal.ofReal ε_pow) :

∃ (c_full : Fin M → Fin n → ℝ) (S : Finset (Fin M)), M / 2 ≤ S.card ∧ (∀ s ∈ S, (MeasureTheory.Measure.pi fun (i : Fin n) => (awgnChannel N h_meas) (c_full s i)) ({ encoder := c_full, decoder := jointTypicalDecoder A c_full }.errorEvent s) ≤ ENNReal.ofReal (4 * ε_d2)) ∧ ∀ s ∈ S, ∑ i : Fin n, c_full s i ^ 2 ≤ ↑n * P

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_capacity_inflatedRate_lt

source

{P P' R'' : ℝ} {N : NNReal} (hP'_pos : 0 < P') (hP'_lt_P : P' ≤ P) (hN_pos : 0 < ↑N) (hR''_lt_C : R'' < 1 / 2 * Real.log (1 + P' / ↑N)) :

R'' < 1 / 2 * Real.log (1 + P / ↑N)

Used by

theorem

InformationTheory.Shannon.AWGN.isAwgnTypicalityHypothesis

source

(P : ℝ) (hP : 0 < P) (N : NNReal) (hN : ↑N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) {R : ℝ} :

0 < R → R < 1 / 2 * Real.log (1 + P / ↑N) → ∀ {ε : ℝ}, 0 < ε → ∃ (N₀ : ℕ), ∀ (n : ℕ), N₀ ≤ n → ∃ (M : ℕ) (_ : ⌈Real.exp (↑n * R)⌉₊ ≤ M) (c : AwgnCode M n P), ∀ (m : Fin M), (c.toCode.errorProbAt (awgnChannel N h_meas) m).toReal < ε

Used by