InformationTheory.Shannon.AWGN.Converse

Imports 6

AWGN channel coding theorem: the converse #

The converse half of the AWGN channel coding theorem (Cover–Thomas): for every power-constrained block code, the rate is bounded by the channel capacity plus the Fano error terms.

The proof follows the standard route:

Fano: log M ≤ I(W; Ŵ) + binEntropy(Pe) + Pe·log(M-1).
Data processing: I(W; Ŵ) ≤ I(Xⁿ; Yⁿ) from the functionality of encoder/decoder.
Chain rule and memorylessness: I(Xⁿ; Yⁿ) ≤ ∑ I(Xᵢ; Yᵢ).
Per-letter max-entropy: I(Xᵢ; Yᵢ) ≤ (1/2) log(1 + P/N).
Summation: log M ≤ n·(1/2) log(1 + P/N) + binEntropy(Pe) + Pe·log(M-1).

Main statements #

awgn_per_letter_mi_bridge_genuine — the per-letter mutual information equals the output differential entropy minus the input-independent noise entropy.
awgn_converse — the converse rate bound for any code with M ≥ 2 messages.

Implementation notes #

The per-letter input marginal perLetterXLaw is a mixture of Diracs over the encoder coordinates, and the per-letter joint (Xᵢ, Yᵢ) law factors as perLetterXLaw ⊗ₘ awgnChannel. The bridge is then obtained from the generic continuous-channel mutual-information chain rule (ChannelCoding.mutualInfoOfChannel_toReal_eq_diffEntropy_sub) together with the translation invariance of the AWGN fiber entropy.
The mixture output law perLetterYLaw has a real density bounded above by the Gaussian peak and below by a single component, which gives the quadratic envelope used to prove integrability of its log-density.

References #

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

The per-letter mutual-information bridge #

noncomputable def

InformationTheory.Shannon.AWGN.perLetterXLaw

source

{P : ℝ} {N : NNReal} (h_meas : IsAwgnChannelMeasurable N) {M n : ℕ} (c : AwgnCode M n P) (i : Fin n) :

MeasureTheory.Measure ℝ

The per-letter input marginal of Xᵢ = c.encoder ω.1 i: the mixture of Diracs (1/M) ∑ₘ δ(c.encoder m i), i.e. the law of the i-th encoder coordinate under a uniform message.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_per_letter_mi_bridge_genuine

source

{P : ℝ} {N : NNReal} (hN : ↑N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) {M n : ℕ} [NeZero M] (c : AwgnCode M n P) (i : Fin n) :

(perLetterMI h_meas c i).toReal = differentialEntropy (perLetterYLaw h_meas c i) - differentialEntropy (ProbabilityTheory.gaussianReal 0 N)

The per-letter mutual information equals the output differential entropy minus the input-independent noise entropy: I(Xᵢ; Yᵢ).toReal = h(Yᵢ) − h(𝒩(0, N)), via the generic continuous-channel mutual-information chain rule and the AWGN translation invariance of the fiber entropy. @audit:ok

Used by

The converse rate bound #

theorem

InformationTheory.Shannon.AWGN.awgn_converse

source

(P : ℝ) (hP : 0 < P) (N : NNReal) (hN : ↑N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) {M n : ℕ} (hM : 2 ≤ M) (hn_pos : 0 < n) (c : AwgnCode M n P) (Pe : ℝ) (hPe : Pe = 1 / ↑M * ∑ m : Fin M, (c.toCode.errorProbAt (awgnChannel N h_meas) m).toReal) :

Real.log ↑M ≤ ↑n * (1 / 2 * Real.log (1 + P / ↑N)) + Real.binEntropy Pe + Pe * Real.log (↑M - 1)

The AWGN converse theorem: for every code with M ≥ 2 messages, block length n, output-power constraint P and average error probability Pe, the rate satisfies

log M ≤ n·(1/2) log(1 + P/N) + binEntropy(Pe) + Pe·log(M - 1).

The per-letter mutual-information bridge is supplied by awgn_per_letter_mi_bridge_genuine, and the rate bound is assembled by awgn_converse_of_perLetterMI_eq_diffEntropy_sub.

Used by