Compactness of stable-attracted walk laws

Prokhorov compactness supplies convergent subsequences of the tight step-path laws (Billingsley, Convergence of Probability Measures, 2nd ed., 1999, Theorem 5.1).

theorem BGW.StableTrees.IsRealStableAttracted.exists_subseq_stepPathLaw {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {T : ℝ} (hT : 0 < T) (q : ℕ → ℕ) : ∃ (P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)) (r : ℕ → ℕ), StrictMono r ∧ Filter.Tendsto (fun (j : ℕ) => stepPathLaw ν T B (q (r j))) Filter.atTop (nhds P)

Every sequence of indices has a subsequence along which the step-path laws converge weakly in ProbabilityMeasure (D T ℝ).

theorem BGW.StableTrees.IsRealStableAttracted.tendsto_norming_floor_ratio {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {t : ℝ} (ht : 0 < t) : Filter.Tendsto (fun (n : ℕ) => B ⌊↑n * t⌋₊ / B n) Filter.atTop (nhds (t ^ (1 / θ)))

Normalizer floor ratio for every t > 0.