AELimit #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Uniform one-sided Gamma tails under almost-everywhere limits #
At a fixed threshold, pointwise convergence puts the target upper-tail event almost everywhere inside the increasing union of the eventual upper-tail events of the approximating sequence. Continuity from below and the uniform tail estimate then preserve the amplitude exactly. The argument is purely set-theoretic and does not require measurability of the random variables.
Main result #
Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_of_ae_tendsto_uniformpreserves a uniform one-sidedGamma_sigmaweak-tail bound under almost-everywhere pointwise convergence.
theorem
Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_of_ae_tendsto_uniform
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{W : ℕ → Ω → ℝ}
{S : Ω → ℝ}
{A σ : ℝ}
(hlim : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => W n ω) Filter.atTop (nhds (S ω)))
(hW : ∀ (n : ℕ), HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (W n) A)
:
A uniform one-sided stretched-exponential tail bound is preserved under almost-everywhere pointwise convergence, with its amplitude unchanged.