InformationTheory.Shannon.AWGN.ConverseCapacityBound

Imports 16

AWGN channel-coding converse — Gaussian capacity bound and assembly #

Builds the capacity-bound layer of the AWGN channel-coding converse (Cover–Thomas): the per-letter input second moment, the per-letter Gaussian maximum-entropy bound, Jensen's inequality, the sum-form capacity bound ∑ᵢ I(Xᵢ; Yᵢ) ≤ n · (1/2) log(1 + P/N), and the final assembly into log M ≤ n · (1/2) log(1 + P/N) + binEntropy(Pe) + Pe · log(M − 1).

Main definitions #

perLetterInputSecondMoment — the per-letter input second moment under a uniform message.

Main statements #

awgn_per_letter_mi_le_log_var — the per-letter Gaussian maximum-entropy bound.
awgn_sum_per_letter_mi_le_n_capacity — ∑ᵢ I(Xᵢ; Yᵢ) ≤ n · (1/2) log(1 + P/N).
awgn_converse_of_perLetterMI_eq_diffEntropy_sub — the assembled converse inequality.

Implementation notes #

The capacity bound is built from a sum form (per-letter second moment, per-letter Gaussian maximum-entropy, and Jensen) rather than a per-letter power constraint, because the per-message power constraint does not yield a per-letter E[Xᵢ²] ≤ P.
h_mi_bridge_per_letter carries the bridge I(Xᵢ; Yᵢ) = h(Yᵢ) − h(Z) as an explicit hypothesis; awgn_per_letter_mi_bridge_genuine (AWGN/Converse.lean) supplies it.

Per-letter input second moment, Jensen, and the sum-form capacity bound #

The capacity bound ∑ᵢ I(Xᵢ; Yᵢ) ≤ n · (1/2) log(1 + P/N) is established in sum form via the per-letter Gaussian maximum-entropy bound and Jensen's inequality, rather than from a per-letter power constraint (which does not follow from the per-message power constraint).

noncomputable def

InformationTheory.Shannon.AWGN.perLetterInputSecondMoment

source

{M n : ℕ} {P : ℝ} (c : AwgnCode M n P) (i : Fin n) :

ℝ

Per-letter input second moment E[Xᵢ² | W ∼ Uniform(Fin M)] = (1/M) ∑ₘ (c.encoder m i)², the second moment of the input letter Xᵢ = c.encoder W i under a uniform message.

Equations

InformationTheory.Shannon.AWGN.perLetterInputSecondMoment c i = 1 / ↑M * ∑ m : Fin M, c.encoder m i ^ 2

Instances For

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_per_letter_input_power_avg

source

{M n : ℕ} (hM_pos : 0 < M) (hn_pos : 0 < n) {P : ℝ} (c : AwgnCode M n P) :

1 / ↑n * ∑ i : Fin n, perLetterInputSecondMoment c i ≤ P

The average of the per-letter input second moments is bounded by P: (1/n) ∑ᵢ E[Xᵢ²] ≤ P, from the per-message power constraint by a Fubini swap.

Used by

Helpers for the per-letter maximum-entropy bound #

theorem

InformationTheory.Shannon.AWGN.awgn_per_letter_mi_le_log_var

source

(P : ℝ) (hP : 0 < P) (N : NNReal) (hN : ↑N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) {M n : ℕ} [NeZero M] (c : AwgnCode M n P) (h_mi_bridge_per_letter : ∀ (i : Fin n), (perLetterMI h_meas c i).toReal = differentialEntropy (perLetterYLaw h_meas c i) - differentialEntropy (ProbabilityTheory.gaussianReal 0 N)) (i : Fin n) :

(perLetterMI h_meas c i).toReal ≤ 1 / 2 * Real.log (1 + perLetterInputSecondMoment c i / ↑N)

Per-letter mutual-information bound via the per-letter input variance: I(Xᵢ; Yᵢ) ≤ (1/2) log(1 + perLetterInputSecondMoment c i / N), derived from the Gaussian maximum-entropy bound differentialEntropy_le_gaussian_of_variance_le. The variance of Yᵢ is at most E[Xᵢ²] + N since the input and the noise are independent, giving

I(Xᵢ; Yᵢ) = h(Yᵢ) − h(gaussianReal 0 N)              -- bridge hypothesis
          ≤ (1/2) log(2πe·v_Y) − (1/2) log(2πe·N)    -- Gaussian maximum entropy
          = (1/2) log(v_Y / N) ≤ (1/2) log((S² + N)/N)
          = (1/2) log(1 + S²/N)

with v_Y := (perLetterInputSecondMoment c i + N).toNNReal.

Used by

theorem

InformationTheory.Shannon.AWGN.sum_log_one_add_le_n_log_one_add_avg

source

{n : ℕ} (hn_pos : 0 < n) (N : ℝ) (hN_pos : 0 < N) (xs : Fin n → ℝ) (hxs_nn : ∀ (i : Fin n), 0 ≤ xs i) :

∑ i : Fin n, 1 / 2 * Real.log (1 + xs i / N) ≤ ↑n * (1 / 2 * Real.log (1 + (1 / ↑n * ∑ i : Fin n, xs i) / N))

Jensen's inequality for the concave map log(1 + ·/N): ∑ᵢ (1/2) log(1 + xᵢ/N) ≤ n · (1/2) log(1 + (∑ᵢ xᵢ / n) / N) for xᵢ ≥ 0.

Real.log is concave on Ioi 0 (Mathlib.Analysis.Convex.SpecificFunctions.Basic. strictConcaveOn_log_Ioi) ⇒ fun x ↦ Real.log (1 + x/N) concave on Ici 0 (composition with affine increasing map, packaged as concaveOn_log_one_add_div in DifferentialEntropy.lean). Apply ConcaveOn.le_map_sum with uniform weights wᵢ := 1/n.

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_sum_per_letter_mi_le_n_capacity

source

(P : ℝ) (hP : 0 < P) (N : NNReal) (hN : ↑N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) {M n : ℕ} [NeZero M] (hn_pos : 0 < n) (c : AwgnCode M n P) (h_mi_bridge_per_letter : ∀ (i : Fin n), (perLetterMI h_meas c i).toReal = differentialEntropy (perLetterYLaw h_meas c i) - differentialEntropy (ProbabilityTheory.gaussianReal 0 N)) :

∑ i : Fin n, (perLetterMI h_meas c i).toReal ≤ ↑n * (1 / 2 * Real.log (1 + P / ↑N))

The sum of per-letter mutual informations is bounded by n · (1/2) log(1 + P/N), combining the per-letter maximum-entropy bound, the average input-power bound, and Jensen's inequality for the concavity of log(1 + ·/N).

Used by

Converse assembly #

theorem

InformationTheory.Shannon.AWGN.awgn_converse_of_perLetterMI_eq_diffEntropy_sub_of_neZero

source

(P : ℝ) (hP : 0 < P) (N : NNReal) (hN : ↑N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) (h_mi_bridge_per_letter : ∀ {M n : ℕ} [NeZero M], 2 ≤ 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)) {M n : ℕ} [NeZero M] (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 assembled converse chain

log M ≤ I(W; Yⁿ).toReal + binEntropy(Pe) + Pe·log(M − 1)     (Fano)
      ≤ I(Xⁿ; Yⁿ).toReal + binEntropy(Pe) + Pe·log(M − 1)    (data-processing)
      ≤ ∑ I(Xᵢ; Yᵢ).toReal + binEntropy(Pe) + Pe·log(M − 1)  (chain rule)
      ≤ n · (1/2) log(1 + P/N) + binEntropy(Pe) + Pe·log(M − 1)  (capacity bound)

The bridge h_mi_bridge_per_letter (per-letter I(Xᵢ; Yᵢ) = h(Yᵢ) − h(Z)) is taken as a hypothesis; awgn_per_letter_mi_bridge_genuine (AWGN/Converse.lean) supplies it.

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_converse_of_perLetterMI_eq_diffEntropy_sub

source

(P : ℝ) (hP : 0 < P) (N : NNReal) (hN : ↑N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) (h_mi_bridge_per_letter : ∀ {M n : ℕ} [NeZero M], 2 ≤ 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)) {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)

Thin wrapper over awgn_converse_of_perLetterMI_eq_diffEntropy_sub_of_neZero: derives the NeZero M instance from 2 ≤ M and delegates. The per-letter identity h_mi_bridge_per_letter is taken as a hypothesis.

Used by