InformationTheory.Shannon.AWGN.BindConvolution

Imports 4

AWGN bind/convolution bridge #

The AWGN kernel composed with the Gaussian input law equals the additive convolution of the input with the noise law, (awgnChannel N h_meas) ∘ₘ (gaussianReal 0 P.toNNReal) = (gaussianReal 0 P.toNNReal) ∗ (gaussianReal 0 N) (IsAwgnBindEqConv). This is a purely measure-theoretic fact that does not depend on the concrete form of the input.

Main statements #

bind_eq_conv_of_translation_kernel — the generic translation-kernel ↔ additive-convolution bridge: for any kernel whose fibers are translation maps of a fixed measure ν, κ ∘ₘ p = p ∗ ν.
isAwgnBindEqConv — the AWGN specialization.

Implementation notes #

The two sides are matched through their lintegral characterizations (Measure.ext_of_lintegral): the Giry-monad composition expands fiberwise via Measure.lintegral_bind, the convolution via Measure.lintegral_conv, and the fibers agree because each AWGN fiber is the translation map of the noise-only Gaussian, gaussianReal x N = (gaussianReal 0 N).map (x + ·) (Mathlib gaussianReal_map_const_add). The AWGN-specific result is the one-line specialization of the generic translation-kernel lemma.

Fiber identity: translation map of a Gaussian #

theorem

InformationTheory.Shannon.AWGN.gaussianReal_eq_map_const_add

source

(N : NNReal) (x : ℝ) :

ProbabilityTheory.gaussianReal x N = MeasureTheory.Measure.map (fun (x_1 : ℝ) => x + x_1) (ProbabilityTheory.gaussianReal 0 N)

Each AWGN fiber is the translation map of the noise-only Gaussian: gaussianReal x N = (gaussianReal 0 N).map (x + ·).

Used by

Generic translation-kernel ↔ convolution bridge #

theorem

InformationTheory.Shannon.AWGN.bind_eq_conv_of_translation_kernel

source

(κ : ProbabilityTheory.Kernel ℝ ℝ) (p ν : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite p] [MeasureTheory.SFinite ν] (hκ : ∀ (x : ℝ), κ x = MeasureTheory.Measure.map (fun (x_1 : ℝ) => x + x_1) ν) :

p.bind ⇑κ = p.conv ν

For any kernel κ : Kernel ℝ ℝ whose every fiber is the translation map of a fixed measure ν (κ x = ν.map (x + ·)), the Giry-monad composition with an s-finite input p coincides with the additive convolution p ∗ ν.

Used by

AWGN specialization #

theorem

InformationTheory.Shannon.AWGN.isAwgnBindEqConv

source

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

IsAwgnBindEqConv P N h_meas

The AWGN kernel composed with the Gaussian input equals the additive convolution with the noise law: (awgnChannel N h_meas) ∘ₘ (gaussianReal 0 P.toNNReal) = (gaussianReal 0 P.toNNReal) ∗ (gaussianReal 0 N).

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_capacity_closed_form_of_maxent_miDecomp

source

(P : ℝ) (hP : 0 < P) (N : NNReal) (hN : ↑N ≠ 0) (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 discharged via the bind/convolution bridge (so IsAwgnBindEqConv is supplied automatically) and the MI decomposition h_decomp, boundedness h_bdd, and max-entropy bound h_max_ent taken as hypotheses.

@audit:superseded-by(awgn_capacity_closed_form_genuine)

Used by