InformationTheory.Shannon.EPI.ApproxIdentityL1

Imports 8

EPI G2 Layer 1 — L¹ convergence of the approximate identity #

For a general L¹ density pX (non-negative, measurable, finite second moment), the convolution with a vanishing Gaussian kernel convDensityAdd pX (gaussianPDFReal 0 ⟨t,_⟩) converges to pX in L¹ as t → 0⁺ (eLpNorm (conv − pX) 1 volume → 0).

Main statements #

convDensityAdd_tendsto_L1_zero: the approximate identity L¹ convergence.

Implementation notes #

The proof assembles three ingredients:

Difference representation via ∫ g_t = 1: (pX ∗ g_t − pX)(z) = ∫ (pX(z−y) − pX(z)) g_t(y) dy.
Continuous Minkowski inequality (L¹, Fubini detour): ‖∫ y, F(·,y) dν‖₁ ≤ ∫ y, ‖F(·,y)‖₁ dν.
L¹ translation continuity and Gaussian concentration (Chebyshev, second moment) via DCT.

noncomputable def

InformationTheory.Shannon.subRightCM

source

(y : ℝ) :

C(ℝ , ℝ )

The right-translation map x ↦ x - y bundled as a C(ℝ, ℝ) element.

Equations

InformationTheory.Shannon.subRightCM y = { toFun := fun (x : ℝ) => x - y, continuous_toFun := ⋯ }

Instances For

Used by

theorem

InformationTheory.Shannon.continuous_subRightCM

source

Continuous subRightCM

Used by

theorem

InformationTheory.Shannon.measurePreserving_subRightCM

source

(y : ℝ) :

MeasureTheory.MeasurePreserving (⇑(subRightCM y)) MeasureTheory.volume MeasureTheory.volume

Used by

theorem

InformationTheory.Shannon.translation_continuous_L1

source

{pX : ℝ → ℝ} (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) :

Filter.Tendsto (fun (y : ℝ) => MeasureTheory.eLpNorm (fun (x : ℝ) => pX (x - y) - pX x) 1 MeasureTheory.volume) (nhds 0) (nhds 0)

L¹ translation continuity: y ↦ eLpNorm (fun x => pX (x - y) - pX x) 1 volume tends to 0 as y → 0. @audit:ok

Used by

theorem

InformationTheory.Shannon.translation_eLpNorm_bound

source

{pX : ℝ → ℝ} (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (y : ℝ) :

MeasureTheory.eLpNorm (fun (x : ℝ) => pX (x - y) - pX x) 1 MeasureTheory.volume ≤ 2 * MeasureTheory.eLpNorm pX 1 MeasureTheory.volume

Bound on the L¹ norm of the translation difference: eLpNorm (· - y) - pX‖₁ ≤ 2 ‖pX‖₁. @audit:ok

Used by

theorem

InformationTheory.Shannon.convDensityAdd_sub_self_eq

source

{pX : ℝ → ℝ} (g : ℝ → ℝ) (hg_one : ∫ (y : ℝ), g y = 1) (z : ℝ) (hi1 : MeasureTheory.Integrable (fun (y : ℝ) => pX (z - y) * g y) MeasureTheory.volume) (hi2 : MeasureTheory.Integrable (fun (y : ℝ) => pX z * g y) MeasureTheory.volume) :

EPIConvDensity.convDensityAdd pX g z - pX z = ∫ (y : ℝ), (pX (z - y) - pX z) * g y

Difference representation: when ∫ g = 1, (pX ∗ g − pX)(z) = ∫ y, (pX(z−y) − pX(z)) · g y. @audit:ok

Used by

theorem

InformationTheory.Shannon.eLpNorm_integral_le_lintegral

source

(F : ℝ → ℝ → ℝ) (ν : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite ν] (hF : AEMeasurable (Function.uncurry F) (MeasureTheory.volume.prod ν)) :

MeasureTheory.eLpNorm (fun (z : ℝ) => ∫ (y : ℝ), F z y ∂ν) 1 MeasureTheory.volume ≤ ∫⁻ (y : ℝ), MeasureTheory.eLpNorm (fun (z : ℝ) => F z y) 1 MeasureTheory.volume ∂ν

Continuous Minkowski inequality (L¹, ℝ≥0∞ form): eLpNorm (fun z => ∫ y, F z y ∂ν) 1 ≤ ∫⁻ y, eLpNorm (fun z => F z y) 1 ∂ν. @audit:ok

Used by

theorem

InformationTheory.Shannon.convDensityAdd_tendsto_L1_zero

source

{pX : ℝ → ℝ} (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (_hpX_mom : MeasureTheory.Integrable (fun (y : ℝ) => y ^ 2 * pX y) MeasureTheory.volume) :

Filter.Tendsto (fun (t : ℝ) => MeasureTheory.eLpNorm (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 t.toNNReal) - pX) 1 MeasureTheory.volume) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Approximate identity L¹ convergence: the convolution with a vanishing Gaussian kernel converges to pX in L¹ norm as t → 0⁺. @audit:ok

Used by