InformationTheory

InformationTheory.Shannon.DeLaValleePoussin

source

Imports 6

The de la Vallée-Poussin criterion for uniform integrability #

A general-purpose, measure-agnostic de la Vallée-Poussin criterion: if there is a superlinear control function G : ℝ≥0∞ → ℝ≥0∞ (meaning G t / t → ∞ as t → ∞) whose composition with the norm has a uniform finite integral bound ∀ i, ∫⁻ x, G ‖f i x‖ₑ ∂μ ≤ C < ∞, then the family f is UnifIntegrable at exponent 1.

This is the classical "forward" direction of the de la Vallée-Poussin theorem. Mathlib does not have this lemma (loogle UnifIntegrable, ConvexOn = Found 0), but the proof is short and reduces to MeasureTheory.unifIntegrable_of — crucially that gateway does not require [IsFiniteMeasure μ], so the criterion applies to infinite measures such as volume.

The intended downstream consumer is the EPI G2 Vitali witness chain for the approximate-identity L¹ convergence of a density under vanishing-variance Gaussian convolution, where μ = volume and f n = negMulLog (pX ∗ g_{u n}).

@audit:ok

def

InformationTheory.Shannon.Superlinear

source
(G : ENNReal → ENNReal) :
Prop

Superlinear growth control, the genuine de la Vallée-Poussin hypothesis on G : ℝ≥0∞ → ℝ≥0∞: for every slope K there is a finite threshold M beyond which K * t ≤ G t. This is the non-degenerate ℝ≥0∞ reading of "G t / t → ∞" — note that Filter.atTop on ℝ≥0∞ collapses to the singleton {∞} (since ∞ is the top), so the literal Tendsto (G ·/·) atTop atTop would be vacuous; this threshold form is the usable statement.

Equations
Instances For
    Used by
      theorem

      InformationTheory.Shannon.unifIntegrable_of_superlinear_lintegral

      source
      {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_2} {f : ι → α → ℝ} (hf : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) (G : ENNReal → ENNReal) (hG_superlinear : Superlinear G) {C : ENNReal} (hC : C ≠ ⊤) (hbound : ∀ (i : ι), ∫⁻ (x : α), G ‖f i x‖ₑ ∂μ ≤ C) :
      MeasureTheory.UnifIntegrable f 1 μ

      The de la Vallée-Poussin criterion (forward direction).

      If G : ℝ≥0∞ → ℝ≥0∞ is superlinear (Superlinear G, i.e. K * t ≤ G t eventually for every slope K) and the family f satisfies a uniform bound ∀ i, ∫⁻ x, G ‖f i x‖ₑ ∂μ ≤ C with C ≠ ∞, then f is uniformly integrable at exponent 1.

      The measure μ is arbitrary — no [IsFiniteMeasure μ] is needed (the proof goes through MeasureTheory.unifIntegrable_of, which is finite-measure-free), so this applies to volume.

      Used by