InformationTheory.Shannon.AWGN.MutualInfoBridge

Imports 3

AWGN output marginal is Gaussian #

The AWGN channel output marginal under Gaussian input is itself Gaussian:

IsAwgnOutputGaussian P N h_meas
  := (outputDistribution (gaussianReal 0 P.toNNReal) (awgnChannel N h_meas))
        = gaussianReal 0 (P.toNNReal + N)

that is, for Y = X + Z with X ∼ 𝒩(0, P) and independent Z ∼ 𝒩(0, N) one has Y ∼ 𝒩(0, P + N).

Main definitions #

IsAwgnBindEqConv — the bridge identity stating that the AWGN kernel composition equals additive convolution of measures.

Main statements #

awgn_output_gaussian_of_bind_eq_conv — the output marginal is 𝒩(0, P + N), given the bind/conv bridge.
awgn_capacity_closed_form_of_maxent_bindconv — the capacity closed form with the output-Gaussian fact reduced to the bind/conv bridge, the remaining mutual-information facts taken as hypotheses.

Implementation notes #

The output marginal is computed in three structural steps: outputDistribution is the second marginal of the joint law (definitional), (p ⊗ₘ W).snd = W ∘ₘ p is the Markov-kernel composition identity (Measure.snd_compProd), and gaussianReal_conv_gaussianReal collapses the convolution of two Gaussians into a single Gaussian.

The middle step — that the AWGN kernel composition coincides with additive convolution — is a generic translation-kernel identity that is independent of the AWGN specifics. Proving it inline through the characteristic-function route would inflate the file by roughly 80–100 lines (lintegral expansion, Fubini, change of variables), so it is exposed as the single named hypothesis IsAwgnBindEqConv and proved separately.

def

InformationTheory.Shannon.AWGN.IsAwgnBindEqConv

source

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

Prop

The bridge identity stating that, for the AWGN translation kernel awgnChannel N and Gaussian input p := gaussianReal 0 P.toNNReal, the kernel composition coincides with the additive convolution of measures:

awgnChannel N ∘ₘ (gaussianReal 0 P.toNNReal)
  = (gaussianReal 0 P.toNNReal) ∗ (gaussianReal 0 N)

This is an AWGN-independent measure-theoretic fact: any translation kernel κ x = ν.map (x + ·) satisfies κ ∘ₘ p = p ∗ ν for s-finite p and finite ν, by Fubini and change of variables. It is exposed as a named hypothesis so the output-Gaussian computation does not have to expand it inline.

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_output_gaussian_of_bind_eq_conv

source

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

IsAwgnOutputGaussian P N h_meas

The AWGN channel output marginal under Gaussian input equals 𝒩(0, P + N), given the bind/conv bridge IsAwgnBindEqConv P N h_meas.

The proof chains outputDistribution = compProd.snd (definitional), Measure.snd_compProd, the bridge hypothesis, and gaussianReal_conv_gaussianReal.

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_capacity_closed_form_of_maxent_bindconv

source

(P : ℝ) (hP : 0 < P) (N : NNReal) (hN : ↑N ≠ 0) (h_bridge : IsAwgnBindEqConv 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, with the output-Gaussian fact reduced to the bind/conv bridge IsAwgnBindEqConv. The mutual-information decomposition (h_decomp), the boundedness h_bdd, and the max-entropy bound (h_max_ent) remain as hypotheses; only the output-Gaussian fact is supplied here.

@audit:superseded-by(awgn_capacity_closed_form_genuine)

Used by