Consequences of quantitative tail bounds

Geometric tail bounds give almost sure convergence, while exponential tail bounds give finite real moments with explicit Gamma-function estimates.

theorem BGW.Probability.ae_tendsto_zero_of_geometric_tails {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (D : ℕ → Ω → ℝ) (hD : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ D n ω) (htail : ∀ (δ : ℝ), 0 < δ → ∃ (C : ℝ) (r : ℝ), 0 ≤ r ∧ r < 1 ∧ ∀ (n : ℕ), μ {ω : Ω | δ < D n ω} ≤ ENNReal.ofReal (C * r ^ n)) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => D n ω) Filter.atTop (nhds 0)

Nonnegative sequences with geometric upper tails converge to zero almost surely.

theorem BGW.Probability.integrable_rpow_of_exp_tail {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (F : Ω → ℝ) (hF : Measurable F) (hF0 : ∀ (ω : Ω), 0 ≤ F ω) {D p : ℝ} (hD : 0 ≤ D) (hp : 0 < p) (htail : ∀ (v : ℝ), 0 ≤ v → μ {ω : Ω | v < F ω} ≤ ENNReal.ofReal (D * Real.exp (-v))) : MeasureTheory.Integrable (fun (ω : Ω) => F ω ^ p) μ ∧ ∫ (ω : Ω), F ω ^ p ∂μ ≤ D * p * Real.Gamma p

Exponential upper tails give finite real moments, with an explicit Gamma bound.