InformationTheory.Shannon.AWGN.AchievabilityAEP

Imports 3

AWGN achievability — continuous AEP engine (Chebyshev concentration) #

False-wall overturn for the awgn-continuous-aep-gaussian wall slug. The continuous AEP mass-concentration sub-bound (i) does not require a.s. convergence (the infinite product measure SLLN that the inventory assumed); a finite-n Chebyshev weak law on the finite product measure Measure.pi (fun _ : Fin n => μ) is enough. Both lemmas below are genuine (0 sorry, sorryAx-free).

Both lemmas are stated abstractly (general probability measure μ + an L² statistic φ), so they can be reused for the AWGN joint law + log-density by substituting the concrete φ.

Mathlib assets used #

ProbabilityTheory.variance_sum_pi — Var[∑ i, fun ω ↦ X i (ω i); pi μ] = ∑ i, Var[X i; μ i].
ProbabilityTheory.meas_ge_le_variance_div_sq — Chebyshev.
MeasureTheory.measurePreserving_eval — each coordinate eval i is measure preserving on pi μ, used via MeasureTheory.integral_map for ν[φ∘eval i] = μ[φ] and MemLp.comp_measurePreserving for MemLp (φ∘eval i) 2 ν.

theorem

InformationTheory.Shannon.AWGN.pi_empirical_mean_concentration

source

{α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] {φ : α → ℝ} (hφ : MeasureTheory.MemLp φ 2 μ) {ε : ℝ} (hε : 0 < ε) {n : ℕ} (hn : 0 < n) :

(MeasureTheory.Measure.pi fun (x : Fin n) => μ) {x : Fin n → α | ε ≤ |(∑ i : Fin n, φ (x i)) / ↑n - ∫ (x : α), φ x ∂μ|} ≤ ENNReal.ofReal (ProbabilityTheory.variance φ μ / (↑n * ε ^ 2))

On the product measure Measure.pi (fun _ : Fin n => μ), the empirical mean (∑ᵢ φ(xᵢ))/n of a common L² statistic φ deviates from μ[φ] by at least ε on a set of mass at most Var[φ]/(n ε²). Finite-n Chebyshev concentration — no infinite product measure / SLLN. This is the engine for the continuous-AEP mass sub-bound (i).

Used by

theorem

InformationTheory.Shannon.AWGN.pi_empirical_mean_typical_mass

source

{α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] {φ : α → ℝ} (hφ : MeasureTheory.MemLp φ 2 μ) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) :

∃ (N₀ : ℕ), ∀ ⦃n : ℕ⦄, N₀ ≤ n → ENNReal.ofReal (1 - η) ≤ (MeasureTheory.Measure.pi fun (x : Fin n) => μ) {x : Fin n → α | |(∑ i : Fin n, φ (x i)) / ↑n - ∫ (x : α), φ x ∂μ| < ε}

From the concentration bound: for any tolerance η > 0 there is a threshold N₀ such that for n ≥ N₀ the empirical mean lands within ε of μ[φ] on a set of mass ≥ 1 - η. The existence form the AEP ultimately consumes.

Used by