Limits of evaluations of stable-attracted paths #
Fixed-jump times are countable. Right approximation by the other times identifies every finite-dimensional distribution of a cluster law, including terminal evaluation (Billingsley, Convergence of Probability Measures, 2nd ed., 1999, Section 13).
theorem
BGW.StableTrees.tendsto_probabilityMeasure_map_of_ae_tendsto
{Ω : Type u_1}
{S : Type u_2}
[MeasurableSpace Ω]
[MetricSpace S]
[MeasurableSpace S]
[BorelSpace S]
(P : MeasureTheory.ProbabilityMeasure Ω)
{g : ℕ → Ω → S}
{f : Ω → S}
(hg : ∀ (n : ℕ), Measurable (g n))
(hf : Measurable f)
(hlim : ∀ᵐ (ω : Ω) ∂↑P, Filter.Tendsto (fun (n : ℕ) => g n ω) Filter.atTop (nhds (f ω)))
:
Filter.Tendsto (fun (n : ℕ) => P.map (g n)) Filter.atTop (nhds (P.map f))
Almost sure pointwise convergence of measurable maps implies convergence of their laws.
theorem
BGW.StableTrees.IsRealStableAttracted.map_increments_of_tendsto
{ν : MeasureTheory.ProbabilityMeasure ℝ}
{θ : ℝ}
{B : ℕ → ℝ}
(h : IsRealStableAttracted ν θ B)
{T : ℝ}
{q : ℕ → ℕ}
(hq : Filter.Tendsto q Filter.atTop Filter.atTop)
{P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)}
(hP : Filter.Tendsto (fun (j : ℕ) => stepPathLaw ν T B (q j)) Filter.atTop (nhds P))
{k : ℕ}
(t : Fin (k + 1) → ↑(Set.Icc 0 T))
(ht : StrictMono t)
:
Every strictly ordered increment vector of a cluster law has the stable product law. The times need not start at zero.