Regular variation of the normalizing sequence (Stage 2)

Source lines 846–853 (inventory B06): under (H_α) the normalizing sequence (a_n) is regularly varying of index 1/α, i.e. a_n / n^{1/α} is slowly varying. The paper cites Feller; here it is derived from the convergence S_n / a_n → Y_α by a convergence-of-types argument on the moduli of characteristic functions:

• BGW.StableTrees.Scalar.tendsto_div_of_tendsto_div: if m'_n / n → κ > 0 then a_n / a_{m'_n} → κ^{-1/α} (Bolzano–Weierstrass on u/(1+u), identification of the limit through |φ(1/a_{m'})|^{m'} = (|φ(u/a_n)|^n)^{m'/n} and |E e^{itY_α}| = exp(cos(πα/2)|t|^α));
• BGW.StableTrees.Scalar.regularlyVaryingSeq: RegularlyVaryingSeq (1/α) a;
• BGW.StableTrees.Scalar.slowlyVarying: x ↦ a_{⌊x⌋} / x^{1/α} is slowly varying;
• BGW.StableTrees.Scalar.tendsto_atTop: a_n → ∞.

No truncated-second-moment criterion is assumed; the proof starts from normalized weak convergence.

Adapted from PoissonDeclumping/Stable/Normalization.lean in igor-kortchemski/rare-subtree-patterns, commit fc5ef722392b1af41e8b9d5fc45d5a521b7823dd (Apache-2.0).

theorem BGW.StableTrees.Scalar.rpow_pow_div {x : ℝ} (hx : 0 ≤ x) {n m : ℕ} (hn : n ≠ 0) : (x ^ n) ^ (↑m / ↑n) = x ^ m

theorem BGW.StableTrees.Scalar.tendsto_natCast_of_div {m' : ℕ → ℕ} {κ : ℝ} (hκ : 0 < κ) (hm' : Filter.Tendsto (fun (n : ℕ) => ↑(m' n) / ↑n) Filter.atTop (nhds κ)) : Filter.Tendsto m' Filter.atTop Filter.atTop

theorem BGW.StableTrees.Scalar.tendsto_div_of_tendsto_div {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) {m' : ℕ → ℕ} {κ : ℝ} (hκ : 0 < κ) (hm' : Filter.Tendsto (fun (n : ℕ) => ↑(m' n) / ↑n) Filter.atTop (nhds κ)) : Filter.Tendsto (fun (n : ℕ) => a n / a (m' n)) Filter.atTop (nhds (κ ^ (-(1 / α))))

Convergence of types for the normalizing sequence: if m'_n / n → κ > 0 then a_n / a_{m'_n} → κ^{-1/α}.

theorem BGW.StableTrees.Scalar.tendsto_div_of_tendsto_div' {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) {m' : ℕ → ℕ} {κ : ℝ} (hκ : 0 < κ) (hm' : Filter.Tendsto (fun (n : ℕ) => ↑(m' n) / ↑n) Filter.atTop (nhds κ)) : Filter.Tendsto (fun (n : ℕ) => a (m' n) / a n) Filter.atTop (nhds (κ ^ (1 / α)))

a_{m'_n} / a_n → κ^{1/α} when m'_n / n → κ > 0.

theorem BGW.StableTrees.Scalar.regularlyVaryingSeq {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : RegularlyVaryingSeq (1 / α) a

Regular variation of (a_n) (source lines 850–851): a_{⌊cn⌋} / a_n → c^{1/α}.

theorem BGW.StableTrees.Scalar.tendsto_atTop {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : Filter.Tendsto a Filter.atTop Filter.atTop

a_n → ∞.

theorem BGW.StableTrees.Scalar.tendsto_succ_div {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : Filter.Tendsto (fun (n : ℕ) => a (n + 1) / a n) Filter.atTop (nhds 1)

a_{n+1} / a_n → 1.

theorem BGW.StableTrees.Scalar.slowlyVarying {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h : StableDomain μ α a) : SlowlyVarying fun (x : ℝ) => a ⌊x⌋₊ / x ^ (1 / α)

a_n / n^{1/α} is slowly varying (source line 850, in the sense of BGW.StableTrees.SlowlyVarying, with a_x := a_{⌊x⌋} for real x).