InformationTheory.Shannon.AWGN.ChannelMeasurability

Imports 3

AWGN kernel measurability #

The AWGN channel kernel fun x : ℝ ↦ gaussianReal x N is measurable on the Giry monad. This discharges the IsAwgnChannelMeasurable N predicate, which lets the AWGN channel coding theorem and the capacity closed form be re-published without the kernel-measurability side hypothesis.

Main statements #

isAwgnChannelMeasurable — the AWGN kernel fun x ↦ gaussianReal x N is measurable.
awgn_channel_coding_theorem_of_isAwgnChannelMeasurable — the AWGN channel coding theorem, with the kernel measurability hypothesis discharged by isAwgnChannelMeasurable.
awgn_capacity_closed_form_of_isAwgnChannelMeasurable — the AWGN capacity closed form, with the kernel measurability hypothesis discharged.

Implementation notes #

The kernel is reshaped as a mean shift of a fixed measure, gaussianReal x N = (gaussianReal 0 N).map (x + ·) (via gaussianReal_map_const_add specialized to mean 0). Measurability of the resulting map then follows structurally from the Giry monad API (Measure.measurable_of_measurable_coe together with Measure.measurable_measure_prodMk_left), rather than from any analytic estimate.

theorem

InformationTheory.Shannon.AWGN.gaussianReal_eq_zero_map

source

(x : ℝ) (N : NNReal) :

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

Used by

theorem

InformationTheory.Shannon.AWGN.isAwgnChannelMeasurable

source

(N : NNReal) :

IsAwgnChannelMeasurable N

The AWGN channel kernel fun x : ℝ ↦ gaussianReal x N is measurable on the Giry monad, discharging the IsAwgnChannelMeasurable N predicate.

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_channel_coding_theorem_of_isAwgnChannelMeasurable

source

(P : ℝ) (hP : 0 < P) (N : NNReal) (hN : ↑N ≠ 0) {R : ℝ} (hR_pos : 0 < R) (hR_lt_C : R < 1 / 2 * Real.log (1 + P / ↑N)) {ε : ℝ} (hε : 0 < ε) :

∃ (N₀ : ℕ), ∀ (n : ℕ), N₀ ≤ n → ∃ (M : ℕ) (_ : ⌈Real.exp (↑n * R)⌉₊ ≤ M) (c : AwgnCode M n P), ∀ (m : Fin M), (c.toCode.errorProbAt (awgnChannel N ⋯) m).toReal < ε

The AWGN channel coding theorem, re-published with the kernel-measurability hypothesis discharged by isAwgnChannelMeasurable N, so it no longer appears in the signature. The body delegates to awgn_channel_coding_theorem.

@audit:ok

Used by

theorem

InformationTheory.Shannon.AWGN.awgn_capacity_closed_form_of_isAwgnChannelMeasurable

source

(P : ℝ) (hP : 0 ≤ P) (N : NNReal) (hN : ↑N ≠ 0) (h_bridge_gauss : (ChannelCoding.mutualInfoOfChannel (ProbabilityTheory.gaussianReal 0 P.toNNReal) (awgnChannel N ⋯)).toReal = 1 / 2 * Real.log (1 + 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 kernel-measurability hypothesis discharged by isAwgnChannelMeasurable N. The remaining hypotheses (h_bridge_gauss, h_bdd, h_max_ent) are unchanged.

@audit:superseded-by(awgn_capacity_closed_form_genuine)

Used by