InformationTheory.Shannon.ParallelGaussian.KKT

Imports 8

Water-filling KKT level and optimality #

The KKT water level and the optimality of the water-filling allocation for the parallel Gaussian channel (Cover–Thomas).

Main statements #

exists_waterFillingKKT_of_pos — for P > 0 and at least one coordinate, a water level ν exists with IsWaterFillingKKT P N ν (the allocation uses up the budget).
isWaterFillingOptimal_of_kkt — given a KKT water level, the water-filling allocation maximizes the constrained per-coordinate log-sum, i.e. IsWaterFillingOptimal P N ν.

Implementation notes #

The existence of the KKT water level is the intermediate value theorem applied to the continuous, monotone ν ↦ ∑_i max(0, ν - N_i). The optimality proof uses the common KKT multiplier λ = 1/(2ν): the per-coordinate tangent upper bound waterFillingCost_tangent_le (from log u ≤ u - 1) summed over coordinates, with complementary slackness and λ ≥ 0 killing the linear remainder.

Continuity and monotonicity of the water-filling sum #

theorem

InformationTheory.Shannon.ParallelGaussian.waterFillingPower_continuous_in_ν

source

{n : ℕ} (N : Fin n → NNReal) (i : Fin n) :

Continuous fun (ν : ℝ) => waterFillingPower ν N i

waterFillingPower ν N i is continuous in ν.

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.waterFillingPower_sum_continuous

source

{n : ℕ} (N : Fin n → NNReal) :

Continuous fun (ν : ℝ) => ∑ i : Fin n, waterFillingPower ν N i

The water-filling total sum ∑_i max(0, ν - N_i) is continuous in ν.

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.waterFillingPower_sum_eq_zero_of_le_min

source

{n : ℕ} (N : Fin n → NNReal) {ν : ℝ} (h : ∀ (i : Fin n), ν ≤ ↑(N i)) :

∑ i : Fin n, waterFillingPower ν N i = 0

At ν ≤ min_i N_i, every coordinate is inactive, so the sum is 0.

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.waterFillingPower_sum_ge_of_all_active

source

{n : ℕ} (N : Fin n → NNReal) {Nmax ν : ℝ} (hNmax : ∀ (i : Fin n), ↑(N i) ≤ Nmax) (hν : Nmax ≤ ν) :

↑n * (ν - Nmax) ≤ ∑ i : Fin n, waterFillingPower ν N i

For ν ≥ Nmax + bound, every coordinate is active and contributes at least ν - Nmax to the sum, giving a sum ≥ n · (ν - Nmax).

Used by

Existence of the KKT water level #

theorem

InformationTheory.Shannon.ParallelGaussian.exists_waterFillingKKT_of_pos

source

{n : ℕ} (P : ℝ) (hP : 0 < P) (N : Fin (n + 1) → NNReal) :

∃ (ν : ℝ), IsWaterFillingKKT P N ν

Existence of a KKT water level. For positive total power P > 0 and at least one coordinate, there is a water level ν whose water-filling allocation exactly uses up the power, ∑_i max(0, ν - N_i) = P.

Used by

Water-filling optimality #

theorem

InformationTheory.Shannon.ParallelGaussian.noise_pos

source

{n : ℕ} (N : Fin n → NNReal) (hN : ∀ (i : Fin n), ↑(N i) ≠ 0) (i : Fin n) :

0 < ↑(N i)

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.waterFillingKKT_level_pos

source

{n : ℕ} (P : ℝ) (hP : 0 < P) (N : Fin n → NNReal) (ν : ℝ) (h_kkt : IsWaterFillingKKT P N ν) :

0 < ν

The KKT water level is positive: 0 < ν. If ν ≤ N_i for every i then every coordinate is inactive and the budget sum is 0 = P, contradicting 0 < P.

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.waterFillingCost_tangent_le

source

{n : ℕ} (N : Fin n → NNReal) (hN : ∀ (i : Fin n), ↑(N i) ≠ 0) (ν : ℝ) (hν : 0 < ν) (i : Fin n) {P'i : ℝ} (hP'i : 0 ≤ P'i) :

1 / 2 * Real.log (1 + P'i / ↑(N i)) ≤ 1 / 2 * Real.log (1 + waterFillingPower ν N i / ↑(N i)) + 1 / (2 * ν) * (P'i - waterFillingPower ν N i)

Per-coordinate tangent (KKT-stationarity) upper bound. For the common KKT multiplier λ = 1/(2ν), the per-coordinate cost g_i(t) = (1/2) log(1 + t/N_i) satisfies g_i(P'_i) ≤ g_i(P*_i) + λ·(P'_i - P*_i) where P*_i = waterFillingPower ν N i.

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.isWaterFillingOptimal_of_kkt

source

{n : ℕ} (P : ℝ) (hP : 0 < P) (N : Fin n → NNReal) (hN : ∀ (i : Fin n), ↑(N i) ≠ 0) (ν : ℝ) (h_kkt : IsWaterFillingKKT P N ν) :

IsWaterFillingOptimal P N ν

Water-filling optimality. Given a KKT water level ν (h_kkt : ∑ max(0, ν - N_i) = P), the water-filling allocation P_i^* = max(0, ν - N_i) maximizes the per-coordinate sum ∑ (1/2) log(1 + P_i / N_i) over the feasible set {P' | ∀ i, 0 ≤ P'_i ∧ ∑_i P'_i ≤ P}, i.e. IsWaterFillingOptimal P N ν.

@audit:ok

Used by