Nonnegative limits with uniform real-integral bounds #
The explicit integrability conclusion prevents default-zero real integrals from standing in for moment bounds when the localization is removed.
References #
- J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.
theorem
BGW.StableTrees.integrable_limit_of_nonneg_integral_le
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{F : ℕ → Ω → ℝ}
{f : Ω → ℝ}
{K : ℝ}
(hK : 0 ≤ K)
(hi : ∀ (n : ℕ), MeasureTheory.Integrable (F n) μ)
(hn : ∀ (n : ℕ), ∀ᵐ (ω : Ω) ∂μ, 0 ≤ F n ω)
(hl : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => F n ω) Filter.atTop (nhds (f ω)))
(hb : ∀ (n : ℕ), ∫ (ω : Ω), F n ω ∂μ ≤ K)
:
Fatou transfers a uniform integral bound to a nonnegative almost sure limit, including integrability of that limit.