AESummability

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Almost-everywhere summability from stretched-exponential layer bounds

The real-valued tsum of a nonsummable fiber is zero, whereas the corresponding sum is infinite. Consequently a weak-Orlicz estimate for the real tsum alone does not identify the actual nonnegative extended-real envelope.

This file supplies the missing analytic bridge. If nonnegative layers have Gamma_sigma bounds at a summable family of positive scales, their first moments are summable. Tonelli's theorem then gives pointwise summability almost everywhere, and the usual ENNReal.ofReal_tsum_of_nonneg identity is available on that full-measure set.

These are general analytic Provider lemmas.

theorem Algsuperdiff.Section3.Provider.Orlicz.ae_summable_of_isBigOWith_gammaSigma {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X : ℕ → Omega → ℝ} {a : ℕ → ℝ} {sigma : ℝ} (hsigma : 0 < sigma) (hX_nonneg : ∀ (n : ℕ) (omega : Omega), 0 ≤ X n omega) (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) mu) (ha : ∀ (n : ℕ), 0 < a n) (ha_summable : Summable a) (hX : ∀ (n : ℕ), HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) (X n) (a n)) : ∀ᵐ (omega : Omega) ∂mu, Summable fun (n : ℕ) => X n omega

A summable family of positive Gamma_sigma scales forces a nonnegative family of random variables to be summable almost everywhere.