InformationTheory.Shannon.ShannonHartley.ConverseFinal

Imports 3

Continuous-time Shannon-Hartley: converse assembly and the identity #

This is the terminal file of the continuous-time band-limited AWGN converse. It bundles the two upstream layers — the fixed-T water-filling real analysis (Waterfill.lean) and the Gaussian rotation / band-Gram ellipsoid (Rotation.lean) — into the converse half contAwgn_le_shannonHartley (≤), and closes the headline identity contAwgn_eq_shannonHartley (=) by le_antisymm against the achievability half contAwgn_ge_shannonHartley.

The route: for a fixed window [0, T] the band-Gram ellipsoid (contAwgn_converse_ellipsoid) gives log M ≤ ∑ᵢ ½log(1 + νᵢQᵢ/(N₀/2)) + Fano, where the νᵢ are the band-Gram eigenvalues; the water-filling split (waterfill_head_tail_bound) with the prolate count (bandGramReal_high_count_le) caps the sum by c₀·TP/N₀ + count·½log(1 + TP/(count·N₀/2)). Dividing by T and letting T → ∞ (waterfill_head_div_tendsto, prolateCount/T → 2W) then c₀ → 0 yields contAwgnRate ε ≤ bandlimitedAwgnCapacity/(1-ε), and the ε → 0 infimum closes the converse.

References #

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

theorem

InformationTheory.Shannon.ShannonHartley.contAwgn_log_le_waterfill

source

{T W N₀ P ε c₀ : ℝ} {M : ℕ} (hN₀ : 0 < N₀) (hP : 0 ≤ P) (hT : 0 < T) (hε0 : 0 < ε) (hε1 : ε < 1) (hc₀0 : 0 < c₀) (hM : 2 ≤ M) (c : ContAwgnCode T W P M) (hce : (c.averageError N₀).toReal ≤ ε) :

Real.log ↑M ≤ (c₀ * (T * P) / N₀ + ↑(TimeBandLimiting.prolateCount T W c₀) * (1 / 2 * Real.log (1 + T * P / (↑(TimeBandLimiting.prolateCount T W c₀) * (N₀ / 2)))) + Real.log 2) / (1 - ε)

Fixed-T converse core: for any code c over [0, T] with average error ≤ ε and at least two messages, log M is capped by the water-filling bound at threshold c₀. Combines the band-Gram ellipsoid, the prolate count domination, and the head/tail water-filling split, then the Fano rearrangement (1-ε)·log M ≤ [waterfill] + log 2.

Used by

theorem

InformationTheory.Shannon.ShannonHartley.waterfill_numerator_nonneg

source

{T W N₀ P c₀ : ℝ} (hN₀ : 0 < N₀) (hP : 0 ≤ P) (hT : 0 < T) (hc₀0 : 0 < c₀) :

0 ≤ c₀ * (T * P) / N₀ + ↑(TimeBandLimiting.prolateCount T W c₀) * (1 / 2 * Real.log (1 + T * P / (↑(TimeBandLimiting.prolateCount T W c₀) * (N₀ / 2)))) + Real.log 2

The water-filling numerator is nonnegative (needed for the sub-threshold message-count branches).

Used by

theorem

InformationTheory.Shannon.ShannonHartley.contAwgn_logMaxMessages_le_waterfill

source

(W N₀ P ε c₀ : ℝ) {T : ℝ} (hW : 0 < W) (hN₀ : 0 < N₀) (hP : 0 ≤ P) (hε0 : 0 < ε) (hε1 : ε < 1) (hc₀0 : 0 < c₀) (hT : 0 < T) :

Real.log ↑(contAwgnMaxMessages T W N₀ P ε) ≤ (c₀ * (T * P) / N₀ + ↑(TimeBandLimiting.prolateCount T W c₀) * (1 / 2 * Real.log (1 + T * P / (↑(TimeBandLimiting.prolateCount T W c₀) * (N₀ / 2)))) + Real.log 2) / (1 - ε)

Per-T message-count bound: log(contAwgnMaxMessages T) is capped by the fixed-T water-filling bound at threshold c₀. Handles the empty / sub-threshold branches (log ≤ 0 ≤ water-filling numerator) and applies contAwgn_log_le_waterfill to the extracted maximizing code.

Used by

theorem

InformationTheory.Shannon.ShannonHartley.waterfill_full_div_tendsto

source

(W N₀ P ε c₀ : ℝ) (hW : 0 < W) (hN₀ : 0 < N₀) (hP : 0 ≤ P) (hε1 : ε < 1) (hc₀0 : 0 < c₀) (hc₀1 : c₀ < 1) :

Filter.Tendsto (fun (T : ℝ) => (c₀ * (T * P) / N₀ + ↑(TimeBandLimiting.prolateCount T W c₀) * (1 / 2 * Real.log (1 + T * P / (↑(TimeBandLimiting.prolateCount T W c₀) * (N₀ / 2)))) + Real.log 2) / (1 - ε) / T) Filter.atTop (nhds ((c₀ * P / N₀ + bandlimitedAwgnCapacity W N₀ P) / (1 - ε)))

The fixed-c₀ water-filling bound divided by T converges as T → ∞ to (c₀·P/N₀ + bandlimitedAwgnCapacity)/(1-ε): the head term c₀·TP/N₀/T is the constant c₀·P/N₀, the count term is waterfill_head_div_tendsto, and log 2 / T → 0.

Used by

theorem

InformationTheory.Shannon.ShannonHartley.contAwgnRate_le

source

(W N₀ P : ℝ) {ε : ℝ} (hW : 0 < W) (hN₀ : 0 < N₀) (hP : 0 ≤ P) (hε0 : 0 < ε) (hε1 : ε < 1) :

contAwgnRate W N₀ P ε ≤ bandlimitedAwgnCapacity W N₀ P / (1 - ε)

The per-ε operational rate is capped by bandlimitedAwgnCapacity/(1-ε): the double limit T → ∞ then c₀ → 0 of the fixed-T water-filling bound.

Used by

theorem

InformationTheory.Shannon.ShannonHartley.contAwgn_le_shannonHartley

source

(W N₀ P : ℝ) (hW : 0 < W) (hN₀ : 0 < N₀) (hP : 0 ≤ P) :

contAwgnOperationalCapacity W N₀ P ≤ bandlimitedAwgnCapacity W N₀ P

The operational capacity of the band-limited AWGN channel is at most the closed form W·log(1 + P/(N₀·W)) — the Shannon-Hartley converse (≤). It is the ε → 0 infimum of the per-ε rate bound contAwgnRate_le.

@audit:ok (#print axioms contAwgn_le_shannonHartley = [propext, Classical.choice, Quot.sound], sorryAx-free; hW/hN₀/hP regularity-only.)

Used by

theorem

InformationTheory.Shannon.ShannonHartley.contAwgn_eq_shannonHartley

source

(W N₀ P : ℝ) (hW : 0 < W) (hN₀ : 0 < N₀) (hP : 0 ≤ P) :

contAwgnOperationalCapacity W N₀ P = bandlimitedAwgnCapacity W N₀ P

The operational capacity of the band-limited AWGN channel equals the closed form W·log(1 + P/(N₀·W)) — the continuous-time Shannon-Hartley formula.

Both halves are proved: achievability (≥) by contAwgn_ge_shannonHartley, and the converse (≤) by contAwgn_le_shannonHartley (band-Gram ellipsoid → prolate-count water-filling → the T → ∞, c₀ → 0, ε → 0 limits). The statement is true as framed over the phantom-free contAwgnOperationalCapacity (the subtype infimum ⨅ ε : ↥(Set.Ioo 0 1)).

Hypotheses hW/hN₀/hP are regularity-only (not load-bearing).

@audit:ok (#print axioms = [propext, Classical.choice, Quot.sound], sorryAx-free — the exact trace identity tsum_prolateEigenvalues_eq (itself sorryAx-free) is off this converse path, which lands via the count domination bandGramReal_high_count_le. Signature scan: both le_antisymm halves are regularity-only, no load-bearing hyp leaks into the identity; the two-sided sandwich over the phantom-free subtype infimum forecloses false-as-framed.)

Used by