InformationTheory

InformationTheory.Shannon.EPI.Vitali.UnifTight

source

Imports 7

EPI G2 Vitali witness — second-moment helpers for the retired UnifTight (UT) route #

This file supplies the second-moment bounds for a Gaussian-convolved density f_n := convDensityAdd pX g_{u n} = pX ∗ g_{u n}: convDensityAdd_second_moment computes ∫ x² f_n = ∫ x² pX + u n (additivity of variance for the independent sum, via the measure-independent Markov inequality mul_meas_ge_le_lintegral, which works on volume with no [IsFiniteMeasure]), and convDensityAdd_second_moment_unif_bdd bounds it uniformly over a bounded positive variance sequence u. The UnifTight witness these bounds originally fed (the tail control for the layer-2 Vitali machinery differentialEntropy_convDensity_integral_tendsto) has since been superseded and removed (see below); convDensityAdd_second_moment remains consumed by the Fatou-LSC route (EPI/G2/KLFatouLSC.lean) and EPI/Vitali/UI.lean.

theorem

InformationTheory.Shannon.convDensityAdd_second_moment

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) {t : ℝ} (ht : 0 < t) :
∫ (x : ℝ), x ^ 2 * EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) x = (∫ (x : ℝ), x ^ 2 * pX x) + (∫ (y : ℝ), pX y) * t

The second moment of a convolution density. For f_t = pX ∗ g_t (Gaussian kernel of variance t): ∫ x², (convDensityAdd pX g_t) ∂volume = (∫ x², pX) + (∫ pX) · t. @audit:ok

Used by
    theorem

    InformationTheory.Shannon.convDensityAdd_second_moment_unif_bdd

    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) (u : ℕ → ℝ) (hu_pos : ∀ (n : ℕ), 0 < u n) (hu_bdd : BddAbove (Set.range u)) :
    ∃ (V : ℝ), ∀ (n : ℕ), ∫ (x : ℝ), x ^ 2 * EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨u n, ⋯⟩) x ≤ V

    A uniform second-moment bound (a genuine sub-structure of the UT witness). For a bounded positive variance sequence u, the second moments ∫ x², f_n = ∫ x² pX + (∫ pX)·u n are uniformly bounded by V := (∫ x² pX) + (∫ pX)·B where B is any upper bound of u. This is the n-uniform majorant that drives the (parked) negMulLog tail estimate. @audit:ok

    Used by

      UT witness removed #

      The Vitali UnifTight witness negMulLog_convDensity_unifTight (the approximate-identity L¹-convergence route) was the layer-2 (differentialEntropy_convDensity_integral_tendsto) input on the Vitali route. The layer-2 body has been re-derived genuinely via the two-sided sandwich (Fatou-LSC (α) limsup upper bound + conditioning (β) per-n lower bound, both @audit:ok), so the Vitali UI/UT witnesses are no longer consumed and the orphan UT witness is deleted. The genuine helpers convDensityAdd_second_moment (still consumed by the (α) machinery and EPI/Vitali/UI.lean) and convDensityAdd_second_moment_unif_bdd are retained.