The stable process law and the functional limit theorem

Tightness and finite-dimensional limits construct the stable Lévy law from the offspring-law witness of exists_stableDomain. Uniqueness then identifies every subsequential limit of an attracted real walk (Billingsley, Convergence of Probability Measures, 2nd ed., 1999, Theorem 13.1; Kallenberg, Foundations of Modern Probability, 2nd ed., 2002, Theorem 16.14).

theorem BGW.StableTrees.IsRealStableAttracted.isStableLevyLaw_of_tendsto {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {T : ℝ} (hT : 0 < 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)) : IsStableLevyLaw θ T P

Any weak limit of step-path laws along indices tending to infinity satisfies IsStableLevyLaw, including the terminal time T and all deterministic times.

Existence, uniqueness and the chosen law

theorem BGW.StableTrees.exists_isStableLevyLaw {θ T : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) : ∃ (P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)), IsStableLevyLaw θ T P

Existence of a stable Lévy law, from the offspring-law witness of exists_stableDomain.

theorem BGW.StableTrees.existsUnique_isStableLevyLaw {θ T : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) : ∃! P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ), IsStableLevyLaw θ T P

Existence and uniqueness (uniqueness is the sealed IsStableLevyLaw.unique).

noncomputable def BGW.StableTrees.stableProcessLaw (θ T : ℝ) : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)

The law of the spectrally positive θ-stable Lévy process on [0,T]; chosen after existence is proved. Junk value (Dirac at the zero path) unless 1 < θ ≤ 2 and 0 < T.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.isStableLevyLaw_stableProcessLaw {θ T : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) : IsStableLevyLaw θ T (stableProcessLaw θ T)

The chosen law satisfies the stable Lévy characterization at valid parameters.

theorem BGW.StableTrees.eq_stableProcessLaw_iff {θ T : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} : P = stableProcessLaw θ T ↔ IsStableLevyLaw θ T P

Characterization: the stable process law is the unique stable Lévy law.

theorem BGW.StableTrees.map_eval_stableProcessLaw {θ T : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) (t : ↑(Set.Icc 0 T)) (ht : 0 < ↑t) : MeasureTheory.Measure.map (fun (f : Skorokhod.D T ℝ) => f t) ↑(stableProcessLaw θ T) = ↑(stableLawAt θ ↑t)

Fixed-time marginals of the stable process law: X_t has law stableLawAt θ t for 0 < t ≤ T.

theorem BGW.StableTrees.ae_eval_zero_stableProcessLaw {θ T : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑(stableProcessLaw θ T), f ⟨0, ⋯⟩ = 0

The stable process law starts at 0 almost surely.

theorem BGW.StableTrees.ae_continuousAt_stableProcessLaw {θ T : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) (t : ↑(Set.Icc 0 T)) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑(stableProcessLaw θ T), ContinuousAt (⇑f) t

No fixed discontinuities for the stable process law (specialization of IsStableLevyLaw.ae_continuousAt).

theorem BGW.StableTrees.map_restrict_stableProcessLaw {θ T a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) (haT : a ≤ T) : (stableProcessLaw θ T).map (Skorokhod.restrict haT) = stableProcessLaw θ a

Consistency of the stable process laws under restriction (specialization of IsStableLevyLaw.map_restrict).

The functional limit theorem

theorem BGW.StableTrees.IsRealStableAttracted.tendsto_stepPathLaw {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {T : ℝ} (hT : 0 < T) : Filter.Tendsto (fun (n : ℕ) => stepPathLaw ν T B n) Filter.atTop (nhds (stableProcessLaw θ T))

Functional limit theorem: for every real iid walk in the domain of attraction (arbitrary eventually positive normalizers, no centering, no monotonicity, no moments) and every horizon T > 0, the laws of the step paths t ↦ S_{⌊nt⌋} / B n, terminal value at T included, converge weakly in D T ℝ to the stable process law.

theorem BGW.StableTrees.IsRealStableAttracted.tendsto_stepPathLaw_subseq {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {T : ℝ} (hT : 0 < T) {q : ℕ → ℕ} (hq : Filter.Tendsto q Filter.atTop Filter.atTop) : Filter.Tendsto (fun (j : ℕ) => stepPathLaw ν T B (q j)) Filter.atTop (nhds (stableProcessLaw θ T))

Subsequence form.

theorem BGW.StableTrees.IsRealStableAttracted.tendsto_map_realStepPath_iid {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {T : ℝ} (hT : 0 < T) {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) (ξ : ℕ → Ω → ℝ) (hξ : ∀ (i : ℕ), Measurable (ξ i)) (hind : ProbabilityTheory.iIndepFun ξ ↑μ) (hlaw : ∀ (i : ℕ), MeasureTheory.Measure.map (ξ i) ↑μ = ↑ν) : Filter.Tendsto (fun (n : ℕ) => μ.map fun (ω : Ω) => Skorokhod.realStepPath T n (B n) fun (i : ℕ) => ξ i ω) Filter.atTop (nhds (stableProcessLaw θ T))

Any measurable iid realization of the steps has the same step-path laws.

theorem BGW.StableTrees.Attraction.IsStableAttracted.tendsto_stepPathLaw {ν : MeasureTheory.Measure ℤ} [MeasureTheory.IsProbabilityMeasure ν] {θ : ℝ} {B : ℕ → ℝ} (h : IsStableAttracted ν θ 0 B) {T : ℝ} (hT : 0 < T) : Filter.Tendsto (fun (n : ℕ) => stepPathLaw (castLaw ν) T B n) Filter.atTop (nhds (stableProcessLaw θ T))

Integer-step corollary through Attraction.IsStableAttracted.isRealStableAttracted (centering 0, eventual positivity of B).

theorem BGW.StableTrees.StableDomain.tendsto_stepPathLaw {μ : PMF ℕ} {θ : ℝ} {a : ℕ → ℝ} (h : StableDomain μ θ a) {T : ℝ} (hT : 0 < T) : Filter.Tendsto (fun (n : ℕ) => stepPathLaw (realOffspringStepLaw μ) T a n) Filter.atTop (nhds (stableProcessLaw θ T))

Offspring corollary: the step K - 1 as a real law, normalizer a of StableDomain.