InformationTheory.Shannon.ShannonHartley.Waterfill

Imports 2

Water-filling arithmetic for the Shannon-Hartley converse #

Pure real-analysis lemmas supporting the continuous-time Shannon-Hartley converse. They are independent of any Gaussian / measure-theoretic / rotation machinery: everything here is elementary calculus on ℝ plus finite-sum concavity (Jensen).

mul_log_one_add_div_monotone — the map x ↦ x · log(1 + a/x) is monotone on (0, ∞) for a ≥ 0 (the per-slot capacity is increasing in the number of degrees of freedom).
waterfill_head_tail_bound — the fixed-T water-filling split: the total per-slot log-capacity is bounded by a tail contribution c₀·TP/N₀ plus a head contribution B · ½ log(1 + TP/(B·N₀/2)), where B dominates the count of "loud" slots.
waterfill_head_div_tendsto — dividing the head contribution by T and letting T → ∞ converges to the Shannon-Hartley capacity bandlimitedAwgnCapacity W N₀ P.

theorem

InformationTheory.Shannon.ShannonHartley.mul_log_one_add_div_monotone

source

{a : ℝ} (ha : 0 ≤ a) :

MonotoneOn (fun (x : ℝ) => x * Real.log (1 + a / x)) (Set.Ioi 0)

The per-slot capacity x ↦ x · log(1 + a/x) is monotone in the number of degrees of freedom x on (0, ∞) for a ≥ 0.

Used by

theorem

InformationTheory.Shannon.ShannonHartley.waterfill_head_tail_bound

source

{k : ℕ} (N₀ TP c₀ : ℝ) (hN₀ : 0 < N₀) (hTP : 0 ≤ TP) (hc₀ : 0 < c₀) (ν Q P' : Fin k → ℝ) (hP'0 : ∀ (i : Fin k), 0 ≤ P' i) (hP'ν : ∀ (i : Fin k), P' i ≤ ν i * Q i) (hQ0 : ∀ (i : Fin k), 0 ≤ Q i) (hQsum : ∑ i : Fin k, Q i ≤ TP) (hν0 : ∀ (i : Fin k), 0 ≤ ν i) (hν1 : ∀ (i : Fin k), ν i ≤ 1) {B : ℕ} (hcount : {i : Fin k | c₀ < ν i}.card ≤ B) :

∑ i : Fin k, 1 / 2 * Real.log (1 + P' i / (N₀ / 2)) ≤ c₀ * TP / N₀ + ↑B * (1 / 2 * Real.log (1 + TP / (↑B * (N₀ / 2))))

The fixed-T water-filling head/tail split. Splitting the slots into "loud" ones (c₀ < νᵢ, at most B of them by the count hypothesis) and "quiet" ones, the total per-slot log-capacity is bounded by a tail term c₀·TP/N₀ (linearization log(1+x) ≤ x on the quiet slots) plus a head term B · ½ log(1 + TP/(B·N₀/2)) (Jensen + monotonicity on the loud slots).

Used by

theorem

InformationTheory.Shannon.ShannonHartley.waterfill_head_div_tendsto

source

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

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

The head water-filling contribution, divided by T, converges to the Shannon-Hartley capacity as T → ∞: prolateCount T W c₀ / T → 2W, and the continuous scaling function y ↦ y · ½ log(1 + P/(y·N₀/2)) evaluated at 2W equals bandlimitedAwgnCapacity W N₀ P.

Used by