InformationTheory.Shannon.AWGN.Basic

Imports 7

AWGN channel capacity #

The continuous specialization of the Shannon noisy-channel coding theorem to the additive white Gaussian noise channel (Cover–Thomas): the power-constrained capacity has the closed form C = (1/2) log(1 + P/N).

Main definitions #

awgnChannel N — the AWGN channel kernel sending input x to the law of Y = x + Z with Z ∼ 𝒩(0, N), i.e. gaussianReal x N.
AwgnCode M n P — a block code with an output-power constraint and a measurable decoder, specialized to alphabet ℝ.
awgnPowerConstraintSet P — the probability measures with lower-integral second moment at most P.
awgnCapacity P N — the supremum of the channel mutual information over inputs in the power-constraint set.

Main statements #

awgnCapacity_eq — the power-constrained capacity equals (1/2) log(1 + P/N), as the sandwich of the Gaussian-achievable lower bound and the max-entropy upper bound.

Implementation notes #

awgnChannel N is defined directly by toFun x := gaussianReal x N, matching the conclusion form of gaussianReal_conv_gaussianReal (mean m₁ + m₂, variance v₁ + v₂). Its kernel measurability field is supplied as the explicit hypothesis IsAwgnChannelMeasurable N rather than constructed inline.
awgnPowerConstraintSet P uses the lower integral ∫⁻ ofReal (x²) ∂p ≤ ofReal P rather than the Bochner ∫ x² ∂p ≤ P. The Bochner integral returns 0 on a non-integrable integrand, so the naive Bochner constraint would admit heavy-tailed inputs with infinite second moment and falsify the converse bound; the lower integral forces genuine integrability of x².
awgnCapacity P N is written as a bare sSup: the stdSimplex form in ChannelCoding/ShannonTheorem.lean assumes a Fintype alphabet and does not apply to the continuous AWGN input.

The AWGN channel kernel #

def

InformationTheory.Shannon.AWGN.IsAwgnChannelMeasurable

source

(N : NNReal) :

Prop

The AWGN measurability hypothesis: (fun x : ℝ => gaussianReal x N) is measurable as a map ℝ → Measure ℝ. This is supplied as an explicit hypothesis so that the kernel can be built without the (not yet available) Mathlib API for mean-measurability of gaussianReal m v.

Equations

InformationTheory.Shannon.AWGN.IsAwgnChannelMeasurable N = Measurable fun (x : ℝ) => ProbabilityTheory.gaussianReal x N

Instances For

Used by

noncomputable def

InformationTheory.Shannon.AWGN.awgnChannel

source

(N : NNReal) (h_meas : IsAwgnChannelMeasurable N) :

ChannelCoding.Channel ℝ ℝ

AWGN channel kernel: on input x : ℝ, the output Y = x + Z with Z ∼ 𝒩(0, N). The kernel returns the law of Y directly as gaussianReal x N (mean shifted to x, variance equal to the noise power N); building it requires IsAwgnChannelMeasurable N.

Equations

InformationTheory.Shannon.AWGN.awgnChannel N h_meas = { toFun := fun (x : ℝ) => ProbabilityTheory.gaussianReal x N, measurable' := h_meas }

Instances For

Used by

theorem

InformationTheory.Shannon.AWGN.awgnChannel_apply

source

@[simp]

(N : NNReal) (h_meas : IsAwgnChannelMeasurable N) (x : ℝ) :

(awgnChannel N h_meas) x = ProbabilityTheory.gaussianReal x N

Used by

instance

InformationTheory.Shannon.AWGN.awgnChannel.instIsMarkovKernel

source

(N : NNReal) (h_meas : IsAwgnChannelMeasurable N) :

ProbabilityTheory.IsMarkovKernel (awgnChannel N h_meas)

awgnChannel N is a Markov kernel (each fibre is a probability measure).

Used by

The AWGN block code #

structure

InformationTheory.Shannon.AWGN.AwgnCode

source

(M n : ℕ) (P : ℝ) :

Type

Block code with a power constraint and a measurable decoder, specialized to input/output alphabet ℝ. Adds the two fields missing from Code M n ℝ ℝ:

decoder_meas — required because MeasurableSingletonClass (Fin n → ℝ) fails for continuous output alphabet (every singleton has Lebesgue measure 0).
power_constraint — the output-power constraint (1/n) ∑ (encoder m i)² ≤ P for every message m.

encoder : Fin M → Fin n → ℝ
decoder : (Fin n → ℝ) → Fin M
decoder_meas : Measurable self.decoder
power_constraint(m : Fin M) : ∑ i : Fin n, self.encoder m i ^ 2 ≤ ↑n * P

Instances For

Used by

noncomputable def

InformationTheory.Shannon.AWGN.AwgnCode.toCode

source

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

ChannelCoding.Code M n ℝ ℝ

Forget the power constraint and decoder measurability to get a bare Code.

Equations

c.toCode = { encoder := c.encoder, decoder := c.decoder }

Instances For

Used by

The power-constraint set and capacity #

def

InformationTheory.Shannon.AWGN.awgnPowerConstraintSet

source

(P : ℝ) :

Set (MeasureTheory.Measure ℝ)

Power constraint set: probability measures with a (genuine, lintegral) second moment ≤ P. Using the lower integral ∫⁻ x, ofReal (x²) ∂p ≤ ofReal P instead of the Bochner ∫ x, x² ∂p ≤ P matters: Bochner ∫ returns 0 on a non-p-integrable integrand (MeasureTheory.integral_undef), so the naive Bochner constraint would admit heavy-tailed inputs (e.g. wide Cauchy laws) with infinite second moment via the spurious ∫ x² ∂p = 0 ≤ P, making the converse bound (1/2)log(1+P/N) false. The lintegral form forces ∫⁻ ofReal(x²) < ∞, hence genuine integrability of x², ruling out those inputs. awgnPowerConstraintSet_mem_iff_integrable bridges back to the Bochner moment + the integrability regularity used by the converse phases.

Equations

InformationTheory.Shannon.AWGN.awgnPowerConstraintSet P = {p : MeasureTheory.Measure ℝ | MeasureTheory.IsProbabilityMeasure p ∧ ∫⁻ (x : ℝ), ENNReal.ofReal (x ^ 2) ∂p ≤ ENNReal.ofReal P}

Instances For

Used by

theorem

InformationTheory.Shannon.AWGN.awgnPowerConstraintSet_mem_iff_integrable

source

(P : ℝ) (hP : 0 ≤ P) (p : MeasureTheory.Measure ℝ) (hp : p ∈ awgnPowerConstraintSet P) :

MeasureTheory.Integrable (fun (x : ℝ) => x ^ 2) p ∧ ∫ (x : ℝ), x ^ 2 ∂p ≤ P

Membership in awgnPowerConstraintSet P (lintegral form) yields both the genuine integrability of x² and the Bochner second-moment bound ∫ x² ∂p ≤ P. This is the bridge the converse phases (AWGN/CapacityConverseMaxent.lean) consume: the lintegral constraint carries the regularity (Integrable (fun x => x²) p) the Bochner form alone cannot supply. @audit:ok

Used by

noncomputable def

InformationTheory.Shannon.AWGN.awgnCapacity

source

(P : ℝ) (N : NNReal) (h_meas : IsAwgnChannelMeasurable N) :

ℝ

Power-constrained channel capacity. Supremum of I(p; W) over probability measures p in awgnPowerConstraintSet P (second moment ≤ P, lintegral form).

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.AWGN.gaussianInput_mem_constraintSet

source

(P : ℝ) (hP : 0 ≤ P) (N : NNReal) :

ProbabilityTheory.gaussianReal 0 P.toNNReal ∈ awgnPowerConstraintSet P

The Gaussian input 𝒩(0, P) lies in the AWGN constraint set awgnPowerConstraintSet P. @audit:ok

Used by

theorem

InformationTheory.Shannon.AWGN.awgnCapacity_ge_gaussian

source

(P : ℝ) (hP : 0 ≤ P) (N : NNReal) (hN : ↑N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) (h_bridge_gauss : (ChannelCoding.mutualInfoOfChannel (ProbabilityTheory.gaussianReal 0 P.toNNReal) (awgnChannel N h_meas)).toReal = 1 / 2 * Real.log (1 + P / ↑N)) (h_bdd : BddAbove ((fun (p : MeasureTheory.Measure ℝ) => (ChannelCoding.mutualInfoOfChannel p (awgnChannel N h_meas)).toReal) '' awgnPowerConstraintSet P)) :

1 / 2 * Real.log (1 + P / ↑N) ≤ awgnCapacity P N h_meas

The AWGN capacity is bounded below by (1/2) log(1 + P/N), achieved by the Gaussian input via the closed-form mutual information hypothesis h_bridge_gauss.

@audit:superseded-by(awgn_capacity_closed_form_genuine)

Used by

theorem

InformationTheory.Shannon.AWGN.awgnCapacity_le_gaussian

source

(P : ℝ) (hP : 0 ≤ P) (N : NNReal) (hN : ↑N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) (h_max_ent : ∀ p ∈ awgnPowerConstraintSet P, (ChannelCoding.mutualInfoOfChannel p (awgnChannel N h_meas)).toReal ≤ 1 / 2 * Real.log (1 + P / ↑N)) :

awgnCapacity P N h_meas ≤ 1 / 2 * Real.log (1 + P / ↑N)

The AWGN capacity is bounded above by (1/2) log(1 + P/N): every input satisfying the second-moment constraint has mutual information at most (1/2) log(1 + P/N) via the Gaussian max-entropy bound h_max_ent.

@audit:superseded-by(awgn_capacity_closed_form_genuine)

Used by

theorem

InformationTheory.Shannon.AWGN.awgnCapacity_eq

source

awgnCapacity P N h_meas = 1 / 2 * Real.log (1 + P / ↑N)

AWGN capacity closed form (Cover–Thomas): the supremum over power-constrained inputs equals (1/2) log(1 + P/N), obtained as the sandwich of the Gaussian-achievable lower bound and the max-entropy upper bound. The hypotheses h_bridge_gauss, h_max_ent, h_bdd carry the closed-form mutual information and boundedness inputs as explicit hypotheses.

@audit:superseded-by(awgn_capacity_closed_form_genuine)

Used by