InformationTheory.Shannon.AWGN.MIBridge

Imports 3

AWGN channel mutual information closed form #

For the AWGN channel Y = X + Z with Gaussian input X ∼ 𝒩(0, P) and independent noise Z ∼ 𝒩(0, N), the channel mutual information has the closed form

I(X ; Y) = h(Y) − h(Y | X) = h(𝒩(0, P + N)) − h(𝒩(0, N)).

This identity is reduced to three explicit primitive predicates, each capturing one fundamental fact about the AWGN structure:

IsAwgnOutputGaussian — the channel output marginal (gaussianReal 0 P ⊗ₘ awgnChannel N).snd = gaussianReal 0 (P+N) (Gaussian + Gaussian convolution).
IsAwgnMIDecomp — the channel MI splits as I(X;Y).toReal = h(Y) − h(Y|X) (mutualInfoOfChannel ↔ entropy bridge), where h(Y|X) := ∫ h(awgnChannel N x) ∂(gaussianReal 0 P) is the integral of fiberwise differential entropies.
IsAwgnCondEntropyEqNoise — the conditional entropy equals the noise entropy: ∫ h(awgnChannel N x) ∂(gaussianReal 0 P) = h(𝒩(0, N)) (translation invariance of differentialEntropy, integrated against the input).

The combinator awgn_mi_bridge_of_primitives chains these three into the closed-form mutual-information identity.

Main definitions #

IsAwgnOutputGaussian, IsAwgnMIDecomp, IsAwgnCondEntropyEqNoise — the three primitive predicates described above.

Main statements #

differentialEntropy_gaussianReal_mean_invariant — h(𝒩(m, v)) = h(𝒩(0, v)).
awgn_cond_entropy_eq_noise_entropy_of_const — discharge of IsAwgnCondEntropyEqNoise.
awgn_mi_bridge_of_primitives — the closed-form mutual information from the three primitives.
awgn_mi_gaussian_closed_form_of_primitives — the (1/2) log(1 + P/N) value of the Gaussian-input mutual information.
awgn_capacity_closed_form_of_primitives — the AWGN capacity closed form with the Gaussian MI fact reduced to two primitives.

Approach #

                                     ┌── IsAwgnOutputGaussian P N h_meas
                                     │   = (jointDistribution ...).snd
                                     │     = gaussianReal 0 (P+N)
mutual-information identity:         │
  I(X;Y).toReal                      ├── IsAwgnMIDecomp P N h_meas
  = h(N(0,P+N)) − h(N(0,N))   ◀────  │   = I(X;Y).toReal
                                     │     = h(output) − h(Y|X)
                                     │
                                     └── IsAwgnCondEntropyEqNoise P N h_meas
                                         = h(Y|X) = h(N(0,N))

Pipeline (proof body of awgn_mi_bridge_of_primitives):

I.toReal = h(out) − h(Y|X)                 -- IsAwgnMIDecomp
         = h(gaussianReal 0 (P+N)) − h(Y|X) -- IsAwgnOutputGaussian (rewrites out)
         = h(gaussianReal 0 (P+N)) − h(N)   -- IsAwgnCondEntropyEqNoise

Implementation notes #

The mean-translation invariance of Gaussian differential entropy, differentialEntropy (gaussianReal m v) = differentialEntropy (gaussianReal 0 v), follows from differentialEntropy_map_add_const and gaussianReal_map_const_add; it is published here as differentialEntropy_gaussianReal_mean_invariant and brings every channel fiber to the noise-only form.

theorem

InformationTheory.Shannon.AWGN.differentialEntropy_gaussianReal_mean_invariant

source

(m : ℝ) {v : NNReal} (hv : v ≠ 0) :

differentialEntropy (ProbabilityTheory.gaussianReal m v) = differentialEntropy (ProbabilityTheory.gaussianReal 0 v)

Mean translation invariance of Gaussian differential entropy: h(𝒩(m, v)) = h(𝒩(0, v)).

Used by

theorem

InformationTheory.Shannon.AWGN.differentialEntropy_awgnChannel_apply_eq_noise

source

(N : NNReal) (hN : N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) (x : ℝ) :

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

Each AWGN channel fiber has the same differential entropy as the noise alone: h(awgnChannel N x) = h(𝒩(0, N)).

Used by

Three primitive predicates #

def

InformationTheory.Shannon.AWGN.IsAwgnOutputGaussian

source

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

Prop

The channel output marginal under Gaussian input gaussianReal 0 P equals the convolution gaussianReal 0 (P + N).

Equations

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

Instances For

Used by

def

InformationTheory.Shannon.AWGN.IsAwgnMIDecomp

source

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

Prop

The channel mutual information splits as I(X;Y) = h(Y) − h(Y|X), where h(Y|X) is the integral of fiberwise differential entropies against the input law. This is the continuous analogue of mutualInfoOfChannel_eq_HX_add_HY_sub_HZ.

Equations

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

Instances For

Used by

def

InformationTheory.Shannon.AWGN.IsAwgnCondEntropyEqNoise

source

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

Prop

The integral of fiberwise differential entropies against the Gaussian input collapses to the noise-only entropy h(𝒩(0, N)).

By differentialEntropy_awgnChannel_apply_eq_noise the integrand is identically the constant h(𝒩(0, N)), so this predicate holds for any probability-measure input; it is kept as a named primitive for symmetry with the other two.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_cond_entropy_eq_noise_entropy_of_const

source

(P : ℝ) (N : NNReal) (hN : N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) :

IsAwgnCondEntropyEqNoise P N h_meas

The integral of fiberwise differential entropies under Gaussian input collapses to h(𝒩(0, N)), discharging IsAwgnCondEntropyEqNoise.

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_mi_bridge_of_primitives

source

(P : ℝ) (N : NNReal) (h_meas : IsAwgnChannelMeasurable N) (h_out : IsAwgnOutputGaussian P N h_meas) (h_decomp : IsAwgnMIDecomp P N h_meas) (h_cond : IsAwgnCondEntropyEqNoise P N h_meas) :

(ChannelCoding.mutualInfoOfChannel (ProbabilityTheory.gaussianReal 0 P.toNNReal) (awgnChannel N h_meas)).toReal = differentialEntropy (ProbabilityTheory.gaussianReal 0 (P.toNNReal + N)) - differentialEntropy (ProbabilityTheory.gaussianReal 0 N)

The closed-form AWGN channel mutual information I(X;Y).toReal = h(𝒩(0, P+N)) − h(𝒩(0, N)), obtained by chaining the three primitive predicates:

I.toReal = h(out) − h(Y|X)                    [IsAwgnMIDecomp]
         = h(𝒩(0, P+N)) − h(Y|X)               [IsAwgnOutputGaussian]
         = h(𝒩(0, P+N)) − h(𝒩(0, N))           [IsAwgnCondEntropyEqNoise]

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_mi_gaussian_closed_form_of_primitives

source

(P : ℝ) (hP_pos : 0 < P) (N : NNReal) (hN : ↑N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) (h_out : IsAwgnOutputGaussian P N h_meas) (h_decomp : IsAwgnMIDecomp P N h_meas) :

(ChannelCoding.mutualInfoOfChannel (ProbabilityTheory.gaussianReal 0 P.toNNReal) (awgnChannel N h_meas)).toReal = 1 / 2 * Real.log (1 + P / ↑N)

The Gaussian-input AWGN channel mutual information equals (1/2) log(1 + P/N), obtained by combining the three primitives into awgn_mi_bridge_of_primitives and running the Gaussian closed-form differentialEntropy_gaussianReal log algebra inline.

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_capacity_closed_form_of_primitives

source

(P : ℝ) (hP : 0 < P) (N : NNReal) (hN : ↑N ≠ 0) (h_out : IsAwgnOutputGaussian P N ⋯) (h_decomp : IsAwgnMIDecomp P N ⋯) (h_bdd : BddAbove ((fun (p : MeasureTheory.Measure ℝ) => (ChannelCoding.mutualInfoOfChannel p (awgnChannel N ⋯)).toReal) '' awgnPowerConstraintSet P)) (h_max_ent : ∀ p ∈ awgnPowerConstraintSet P, (ChannelCoding.mutualInfoOfChannel p (awgnChannel N ⋯)).toReal ≤ 1 / 2 * Real.log (1 + P / ↑N)) :

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

The AWGN capacity closed form, re-published with the Gaussian mutual-information fact reduced to the two primitives IsAwgnOutputGaussian and IsAwgnMIDecomp. The remaining hypotheses (h_bdd, h_max_ent) are unchanged.

@audit:superseded-by(awgn_capacity_closed_form_genuine)

Used by