Compact square-mean convergence to the auxiliary clock #
Fatou transfers the compact Cauchy bounds to the raw auxiliary limit, including integrability at every positive cutoff.
References #
- [J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV]
theorem
BGW.StableTrees.integrable_ae_limit_of_integral_le
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{G : ℕ → Ω → ℝ}
{F : Ω → ℝ}
{C : ℝ}
(hG : ∀ (k : ℕ), MeasureTheory.Integrable (G k) μ)
(hG0 : ∀ (k : ℕ), ∀ᵐ (f : Ω) ∂μ, 0 ≤ G k f)
(hF0 : ∀ᵐ (f : Ω) ∂μ, 0 ≤ F f)
(hC : 0 ≤ C)
(hlim : ∀ᵐ (f : Ω) ∂μ, Filter.Tendsto (fun (k : ℕ) => G k f) Filter.atTop (nhds (F f)))
(hb : ∀ᶠ (k : ℕ) in Filter.atTop, ∫ (f : Ω), G k f ∂μ ≤ C)
:
Fatou's lemma with an eventual uniform bound for nonnegative real integrals.
theorem
BGW.StableTrees.supOccupation_compact_L2_tendsto_supAuxLimit
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(T : NNReal)
:
(∀ (ε : ℝ),
0 < ε →
MeasureTheory.Integrable
(fun (f : Skorokhod.DLoc) => (⨆ (t : ↑(Set.Iic T)), |supOccupation ε f ↑t - supAuxLimit θ f ↑t|) ^ 2)
↑(stableLocalLaw θ)) ∧ Filter.Tendsto
(fun (ε : ℝ) =>
∫ (f : Skorokhod.DLoc), (⨆ (t : ↑(Set.Iic T)), |supOccupation ε f ↑t - supAuxLimit θ f ↑t|) ^ 2 ∂↑(stableLocalLaw θ))
(nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
Full-filter compact L² convergence O_ε → M^* as ε ↓ 0 (not only along
supAuxEps): Cauchy estimate plus Fatou along the fast subsequence.
theorem
BGW.StableTrees.integrable_sq_of_ae_tendsto_of_integral_sq_le
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{F : Ω → ℝ}
{G : ℕ → Ω → ℝ}
{C : ℝ}
(hF : MeasureTheory.AEStronglyMeasurable F μ)
(hG : ∀ (k : ℕ), MeasureTheory.Integrable (fun (f : Ω) => G k f ^ 2) μ)
(hC : 0 ≤ C)
(hlim : ∀ᵐ (f : Ω) ∂μ, Filter.Tendsto (fun (k : ℕ) => G k f) Filter.atTop (nhds (F f)))
(hb : ∀ (k : ℕ), ∫ (f : Ω), G k f ^ 2 ∂μ ≤ C)
:
MeasureTheory.Integrable (fun (f : Ω) => F f ^ 2) μ
A square-integrable sequence with uniformly bounded second moments has a square-integrable almost sure limit.
theorem
BGW.StableTrees.integrable_sq_supAuxLimit
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(T : NNReal)
:
MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => supAuxLimit θ f T ^ 2) ↑(stableLocalLaw θ)
The auxiliary clock has square integrable values on every compact horizon.