Normalizer bounds for real stable attraction

The normalizer diverges, and its ratio theorem is uniform on compact ranges of index ratios. Dyadic chaining then gives Potter bounds without assuming that the normalizer is monotone.

References: W. Feller, An Introduction to Probability Theory and Its Applications, vol. II, ch. XVII; N. H. Bingham, C. M. Goldie and J. L. Teugels, Regular Variation (1987), §1.5 (Potter bounds).

theorem BGW.StableTrees.IsRealStableAttracted.tendsto_norming_atTop {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) : Filter.Tendsto B Filter.atTop Filter.atTop

The normalizer diverges: B n → +∞, without monotonicity.

theorem BGW.StableTrees.IsRealStableAttracted.uniform_ratio {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) (ε : ℝ) : ε > 0 → ∃ (N : ℕ), ∀ n ≥ N, ∀ (m : ℕ), a * ↑n ≤ ↑m → ↑m ≤ b * ↑n → |B m / B n - (↑m / ↑n) ^ (1 / θ)| ≤ ε

Uniform convergence of the ratio on compact index ranges.

theorem BGW.StableTrees.IsRealStableAttracted.potter_upper {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {ε' A : ℝ} (hε' : 0 < ε') (hA : 1 < A) : ∃ (N : ℕ), ∀ n ≥ N, ∀ m ≥ N, B m / B n ≤ A * max ((↑m / ↑n) ^ (1 / θ + ε')) ((↑m / ↑n) ^ (1 / θ - ε'))

Potter-type upper bound without monotonicity: for every ε' > 0 and every A > 1, for all large indices m, n (both ≥ N), B m / B n ≤ A * max ((m/n)^(1/θ + ε')) ((m/n)^(1/θ - ε')).

theorem BGW.StableTrees.IsRealStableAttracted.potter_lower {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {ε' A : ℝ} (hε' : 0 < ε') (hA : 1 < A) : ∃ (N : ℕ), ∀ n ≥ N, ∀ m ≥ N, A⁻¹ * min ((↑m / ↑n) ^ (1 / θ + ε')) ((↑m / ↑n) ^ (1 / θ - ε')) ≤ B m / B n

Potter-type lower bound: same hypotheses, B m / B n ≥ A⁻¹ * min (…) (…).

theorem BGW.StableTrees.IsRealStableAttracted.small_index_ratio {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) (ε : ℝ) : ε > 0 → ∃ δ > 0, ∃ (N : ℕ), ∀ n ≥ N, ∀ (m : ℕ), 1 ≤ m → ↑m ≤ δ * ↑n + 2 → |B m / B n| ≤ ε

Uniformly small ratios for small positive indices (Node 5), in absolute value: finitely many indices with nonpositive normalizer values are absorbed by the divergence of B n.

theorem BGW.StableTrees.IsRealStableAttracted.bounded_index_ratio {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) (A : ℝ) : ∃ C > 0, ∃ (N : ℕ), ∀ n ≥ N, ∀ (m : ℕ), 1 ≤ m → ↑m ≤ A * ↑n + 2 → |B m / B n| ≤ C

Bounded ratios on finite time windows (Node 5), in absolute value.