InformationTheory.Shannon.ParallelGaussian.Basic

Imports 7

Parallel Gaussian channels and water-filling #

The capacity of n parallel AWGN channels Y_i = X_i + Z_i, Z_i ∼ 𝒩(0, N_i) (i : Fin n) under the total power constraint ∑_i E[X_i²] ≤ P, and its water-filling solution (Cover–Thomas).

Main definitions #

parallelGaussianChannel N — the product Markov kernel on Fin n → ℝ whose i-th output coordinate is X_i + Z_i with Z_i ∼ 𝒩(0, N_i), independent across coordinates.
waterFillingPower ν N — the water-filling power allocation i ↦ max(0, ν - N_i) for water level ν.
parallelGaussianCapacity P N — the power-constrained information capacity, the sSup of the mutual information over inputs in parallelGaussianPowerConstraintSet P.
parallelGaussianPowerConstraintSet P — the probability measures with total per-coordinate second moment ≤ P, in lower-integral form.
waterFillingActiveSet ν N — the coordinates {i | N_i < ν} allocated positive power.

Main statements #

parallelGaussianPowerConstraintSet_mem_iff_integrable — membership yields genuine per-coordinate integrability of (x i)² together with the Bochner second-moment bound.

Implementation notes #

parallelGaussianChannel is defined directly as toFun x := Measure.pi (fun i ↦ gaussianReal (x i) (N i)), matching the conclusion form of Measure.pi_pi; its measurability is supplied as the hypothesis IsParallelGaussianKernelMeasurable N.
waterFillingPower uses max 0 (ν - N_i), matching max_eq_left / max_eq_right / le_max_left.
The power constraint uses the lower integral ∑_i ∫⁻ ofReal ((x i)²) ∂p ≤ ofReal P rather than the Bochner ∑_i ∫ (x i)² ∂p ≤ P. Bochner ∫ returns 0 on a non-integrable integrand, so the naive Bochner constraint would admit heavy-tailed inputs with infinite second moment; the lower integral forces genuine integrability of every (x i)².

References #

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

Parallel Gaussian channel kernel #

def

InformationTheory.Shannon.ParallelGaussian.IsParallelAwgnChannelMeasurable

source

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

Prop

Per-coordinate AWGN measurability hypothesis, bundled over Fin n.

Equations

InformationTheory.Shannon.ParallelGaussian.IsParallelAwgnChannelMeasurable N = ∀ (i : Fin n), InformationTheory.Shannon.AWGN.IsAwgnChannelMeasurable (N i)

Instances For

Used by

def

InformationTheory.Shannon.ParallelGaussian.IsParallelGaussianKernelMeasurable

source

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

Prop

Measurability of the parallel kernel map x : Fin n → ℝ ↦ Measure.pi (fun i ↦ gaussianReal (x i) (N i)), supplied as a hypothesis.

Equations

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

Instances For

Used by

noncomputable def

InformationTheory.Shannon.ParallelGaussian.parallelGaussianChannel

source

{n : ℕ} (N : Fin n → NNReal) (h_meas : IsParallelAwgnChannelMeasurable N) (h_parallel_meas : IsParallelGaussianKernelMeasurable N) :

ChannelCoding.Channel (Fin n → ℝ) (Fin n → ℝ)

The parallel Gaussian channel kernel: on input x : Fin n → ℝ the output y : Fin n → ℝ has y i = x i + z i with z i ∼ 𝒩(0, N i) independent across coordinates. The output law is the product measure Measure.pi (fun i ↦ gaussianReal (x i) (N i)).

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.parallelGaussianChannel_apply

source

@[simp]

{n : ℕ} (N : Fin n → NNReal) (h_meas : IsParallelAwgnChannelMeasurable N) (h_parallel_meas : IsParallelGaussianKernelMeasurable N) (x : Fin n → ℝ) :

(parallelGaussianChannel N h_meas h_parallel_meas) x = MeasureTheory.Measure.pi fun (i : Fin n) => ProbabilityTheory.gaussianReal (x i) (N i)

Used by

instance

InformationTheory.Shannon.ParallelGaussian.parallelGaussianChannel.instIsMarkovKernel

source

{n : ℕ} (N : Fin n → NNReal) (h_meas : IsParallelAwgnChannelMeasurable N) (h_parallel_meas : IsParallelGaussianKernelMeasurable N) :

ProbabilityTheory.IsMarkovKernel (parallelGaussianChannel N h_meas h_parallel_meas)

parallelGaussianChannel N is a Markov kernel (each fiber is a product of probability measures, hence itself a probability measure).

Used by

Water-filling power allocation #

noncomputable def

InformationTheory.Shannon.ParallelGaussian.waterFillingPower

source

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

Fin n → ℝ

The water-filling power allocation: for water level ν : ℝ and noise vector N : Fin n → ℝ≥0, coordinate i is allocated max(0, ν - N_i).

Equations

InformationTheory.Shannon.ParallelGaussian.waterFillingPower ν N i = max 0 (ν - ↑(N i))

Instances For

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.waterFillingPower_apply

source

@[simp]

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

waterFillingPower ν N i = max 0 (ν - ↑(N i))

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.waterFillingPower_nonneg

source

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

0 ≤ waterFillingPower ν N i

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.waterFillingPower_eq_zero_of_inactive

source

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

waterFillingPower ν N i = 0

An inactive coordinate (ν ≤ N_i) is allocated zero power.

Used by

Parallel Gaussian capacity #

def

InformationTheory.Shannon.ParallelGaussian.parallelGaussianPowerConstraintSet

source

{n : ℕ} (P : ℝ) :

Set (MeasureTheory.Measure (Fin n → ℝ))

The parallel power constraint set: probability measures with total per-coordinate second moment ≤ P, in lower-integral form ∑_i ∫⁻ ofReal ((x i)²) ∂p ≤ ofReal P. Multivariate analogue of AWGN.awgnPowerConstraintSet. The lower-integral form forces each ∫⁻ ofReal ((x i)²) < ∞, hence genuine integrability of every coordinate (x i)² (a Bochner ∫ constraint would spuriously admit heavy-tailed inputs with infinite second moment).

@audit:ok

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.parallelGaussianPowerConstraintSet_mem_iff_integrable

source

{n : ℕ} (P : ℝ) (hP : 0 ≤ P) (p : MeasureTheory.Measure (Fin n → ℝ)) (hp : p ∈ parallelGaussianPowerConstraintSet P) :

(∀ (i : Fin n), MeasureTheory.Integrable (fun (x : Fin n → ℝ) => x i ^ 2) p) ∧ ∑ i : Fin n, ∫ (x : Fin n → ℝ), x i ^ 2 ∂p ≤ P

Membership in parallelGaussianPowerConstraintSet P (lintegral form) yields both the genuine per-coordinate integrability of (x i)² and the Bochner total second-moment bound ∑_i ∫ (x i)² ∂p ≤ P. Multivariate analogue of AWGN.awgnPowerConstraintSet_mem_iff_integrable; the lintegral constraint carries the regularity (Integrable (fun x ↦ (x i)²) p) the Bochner form alone cannot supply. @audit:ok

Used by

noncomputable def

InformationTheory.Shannon.ParallelGaussian.parallelGaussianCapacity

source

{n : ℕ} (P : ℝ) (N : Fin n → NNReal) (h_meas : IsParallelAwgnChannelMeasurable N) (h_parallel_meas : IsParallelGaussianKernelMeasurable N) :

ℝ

The power-constrained parallel Gaussian capacity: the supremum of the mutual information I(p; parallelGaussianChannel N) over inputs p in parallelGaussianPowerConstraintSet P.

Equations

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

Instances For

Used by

Water-filling KKT, optimality, and per-coordinate reduction predicates #

def

InformationTheory.Shannon.ParallelGaussian.IsWaterFillingKKT

source

{n : ℕ} (P : ℝ) (N : Fin n → NNReal) (ν : ℝ) :

Prop

The water-filling KKT condition: the water level ν uses up the total budget, ∑_i max(0, ν - N_i) = P. For the unconstrained water-filling problem this characterizes the KKT-optimal Lagrange multiplier (a unique such ν exists by the intermediate value theorem).

Equations

InformationTheory.Shannon.ParallelGaussian.IsWaterFillingKKT P N ν = (∑ i : Fin n, InformationTheory.Shannon.ParallelGaussian.waterFillingPower ν N i = P)

Instances For

Used by

def

InformationTheory.Shannon.ParallelGaussian.IsWaterFillingOptimal

source

{n : ℕ} (P : ℝ) (N : Fin n → NNReal) (ν : ℝ) :

Prop

Water-filling optimality: the water-filling allocation P_i^* = max(0, ν - N_i) maximizes the per-coordinate sum ∑ (1/2) log(1 + P_i/N_i) subject to P_i ≥ 0, ∑ P_i ≤ P.

Equations

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

Instances For

Used by

def

InformationTheory.Shannon.ParallelGaussian.IsParallelGaussianPerCoordReduction

source

{n : ℕ} (P : ℝ) (N : Fin n → NNReal) (h_meas : IsParallelAwgnChannelMeasurable N) (h_parallel_meas : IsParallelGaussianKernelMeasurable N) (ν : ℝ) :

Prop

The per-coordinate water-filling reduction: the parallel Gaussian capacity equals the per-coordinate water-filling sum ∑_i (1/2) log(1 + max(0, ν - N_i) / N_i).

This predicate is the capacity equality itself, so it is intended to be derived (not taken as a hypothesis).

See also isParallelGaussianPerCoordReduction_of_kkt.

Equations