Analytic consequences of regular variation of the normalizing sequence

Consequences of regular variation of (a_n) used in the source (lines 1015–1050, 1080–1110, 1136–1251, 1747–1790, 2233–2298), for a monotone a : ℕ → ℝ, positive at n ≥ 1, with RegularlyVaryingSeq ρ a:

• tendsto_ratio_of_tendsto_div: if k n / n → c > 0 then a (k n) / a n → c ^ ρ (covers a_{⌊εn⌋}/a_n → ε^ρ, a_{n-o(n)}/a_n → 1, a_{n-1}/a_n → 1).
• eventually_rpow_le_le: a_n = n^{ρ+o(1)}.
• tendsto_div_self, tendsto_atTop, exists_le_mul, exists_le_mul_of_le_mul: a_n = o(n), a_n → ∞, a_n ≤ C n, and a_y ≤ C a_x whenever y ≤ K x.
• tendsto_ratio_zero_of_isLittleO: M_n = o(n) gives a_{M_n} / a_n → 0.
• tendsto_sub_ratio, tendsto_add_ratio, eventually_uniform_sub_add: a_{n ∓ m_n} / a_n → 1 for m_n = o(n), uniformly over m ≤ M_n.
• tendsto_sqrt_div: for r_n = √(a_{M_n} a_n), r_n / a_{M_n} → ∞ and r_n / a_n → 0.
• eventually_floor_rpow_bounds, eventually_floor_rpow_div_le, eventually_div_floor_rpow_le: polynomial cutoffs M_n = ⌊n^θ⌋₊.
• tendsto_mul_div_floor_rpow, tendsto_div_floor_rpow: the two limits in the proof of Lemma lem:critM (source lines 1087–1105), for an n^{o(1)} numerator.

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

theorem BGW.StableTrees.half_le_natFloor {x : ℝ} (hx : 1 ≤ x) : x / 2 ≤ ↑⌊x⌋₊

⌊x⌋₊ ≥ x / 2 for x ≥ 1.

theorem BGW.StableTrees.tendsto_zero_of_le_mul_rpow {l : Filter ℕ} (hl : l ≤ Filter.atTop) {f : ℕ → ℝ} {C γ : ℝ} (hγ : γ < 0) (h0 : ∀ᶠ (n : ℕ) in l, 0 ≤ f n) (h : ∀ᶠ (n : ℕ) in l, f n ≤ C * ↑n ^ γ) : Filter.Tendsto f l (nhds 0)

If 0 ≤ f n ≤ C n ^ γ eventually along l ≤ atTop, with γ < 0, then f → 0 along l.

theorem BGW.StableTrees.RegularlyVaryingSeq.tendsto_ratio_of_tendsto_div {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) {k : ℕ → ℕ} {c : ℝ} (hc : 0 < c) (hk : Filter.Tendsto (fun (n : ℕ) => ↑(k n) / ↑n) Filter.atTop (nhds c)) : Filter.Tendsto (fun (n : ℕ) => a (k n) / a n) Filter.atTop (nhds (c ^ ρ))

If k n / n → c > 0, then a (k n) / a n → c ^ ρ.

theorem BGW.StableTrees.RegularlyVaryingSeq.tendsto_floor_mul {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) {ε : ℝ} (hε : 0 < ε) : Filter.Tendsto (fun (n : ℕ) => a ⌊ε * ↑n⌋₊ / a n) Filter.atTop (nhds (ε ^ ρ))

For fixed ε > 0, a ⌊ε n⌋₊ / a n → ε ^ ρ (the definition, restated).

theorem BGW.StableTrees.RegularlyVaryingSeq.eventually_rpow_le_le {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 ≤ ρ) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, ↑n ^ (ρ - δ) ≤ a n ∧ a n ≤ ↑n ^ (ρ + δ)

a_n = n^{ρ + o(1)}: for every δ > 0, eventually n^(ρ-δ) ≤ a n ≤ n^(ρ+δ).

theorem BGW.StableTrees.RegularlyVaryingSeq.tendsto_atTop {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 < ρ) : Filter.Tendsto a Filter.atTop Filter.atTop

a n → ∞ (positive index).

theorem BGW.StableTrees.RegularlyVaryingSeq.tendsto_div_self {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) : Filter.Tendsto (fun (n : ℕ) => a n / ↑n) Filter.atTop (nhds 0)

a_n = o(n) (index ρ < 1): a n / n → 0.

theorem BGW.StableTrees.RegularlyVaryingSeq.exists_le_mul {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → a n ≤ C * ↑n

a n ≤ C n for all n ≥ 1 (index ρ < 1).

theorem BGW.StableTrees.RegularlyVaryingSeq.exists_le_mul_of_le_mul {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 ≤ ρ) (K : ℝ) : ∃ (C : ℝ), 0 < C ∧ ∀ (x y : ℕ), 1 ≤ x → ↑y ≤ K * ↑x → a y ≤ C * a x

Comparability: for every K, there is C > 0 with a y ≤ C a x whenever 1 ≤ x and y ≤ K x (e.g. a_q ≍ a_n for n/2 ≤ q ≤ n).

theorem BGW.StableTrees.RegularlyVaryingSeq.tendsto_ratio_zero_of_isLittleO {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 < ρ) {M : ℕ → ℕ} (hM : (fun (n : ℕ) => ↑(M n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) : Filter.Tendsto (fun (n : ℕ) => a (M n) / a n) Filter.atTop (nhds 0)

If M_n = o(n) then a (M n) / a n → 0 (positive index).

theorem BGW.StableTrees.RegularlyVaryingSeq.tendsto_sub_ratio {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) {m : ℕ → ℕ} (hm : (fun (n : ℕ) => ↑(m n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) : Filter.Tendsto (fun (n : ℕ) => a (n - m n) / a n) Filter.atTop (nhds 1)

a_{n - m_n} / a_n → 1 for m_n = o(n) (natural subtraction).

theorem BGW.StableTrees.RegularlyVaryingSeq.tendsto_add_ratio {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) {m : ℕ → ℕ} (hm : (fun (n : ℕ) => ↑(m n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) : Filter.Tendsto (fun (n : ℕ) => a (n + m n) / a n) Filter.atTop (nhds 1)

a_{n + m_n} / a_n → 1 for m_n = o(n).

theorem BGW.StableTrees.RegularlyVaryingSeq.eventually_uniform_sub_add {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) {M : ℕ → ℕ} (hM : (fun (n : ℕ) => ↑(M n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ j ≤ M n, (1 - ε) * a n ≤ a (n - j) ∧ a (n - j) ≤ a n ∧ a n ≤ a (n + j) ∧ a (n + j) ≤ (1 + ε) * a n

Uniform version: for M_n = o(n) and ε > 0, eventually for all j ≤ M n, (1-ε) a n ≤ a (n-j) ≤ a n ≤ a (n+j) ≤ (1+ε) a n.

theorem BGW.StableTrees.RegularlyVaryingSeq.tendsto_sqrt_div {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 < ρ) {M : ℕ → ℕ} (hMtop : Filter.Tendsto M Filter.atTop Filter.atTop) (hM : (fun (n : ℕ) => ↑(M n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) : Filter.Tendsto (fun (n : ℕ) => √(a (M n) * a n) / a (M n)) Filter.atTop Filter.atTop ∧ Filter.Tendsto (fun (n : ℕ) => √(a (M n) * a n) / a n) Filter.atTop (nhds 0)

Source lines 1747–1750: with r_n = √(a_{M_n} a_n), M_n → ∞ and M_n = o(n), r_n / a_{M_n} → ∞ and r_n / a_n → 0.

theorem BGW.StableTrees.RegularlyVaryingSeq.eventually_floor_rpow_bounds {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 < ρ) {θ δ : ℝ} (hθ : 0 < θ) (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, ↑n ^ (θ * ρ - δ) ≤ a ⌊↑n ^ θ⌋₊ ∧ a ⌊↑n ^ θ⌋₊ ≤ ↑n ^ (θ * ρ + δ)

Polynomial cutoffs: for θ > 0 and δ > 0, eventually n^(θρ - δ) ≤ a ⌊n^θ⌋₊ ≤ n^(θρ + δ), i.e. a_{⌊n^θ⌋} = n^{θρ + o(1)}.

theorem BGW.StableTrees.RegularlyVaryingSeq.eventually_floor_rpow_div_le {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 < ρ) {η δ : ℝ} (hη : η < 1) (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, a ⌊↑n ^ (1 - η)⌋₊ / a n ≤ ↑n ^ (-(ρ * η) + δ)

Polynomial cutoff M_n = ⌊n^(1-η)⌋₊, η < 1: for every δ > 0, eventually a_{M_n} / a_n ≤ n^(-ρη + δ).

theorem BGW.StableTrees.RegularlyVaryingSeq.eventually_div_floor_rpow_le {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 ≤ ρ) {θ δ : ℝ} (hθ : 0 < θ) (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, a n / ↑⌊↑n ^ θ⌋₊ ≤ ↑n ^ (ρ - θ + δ)

Polynomial cutoff M_n = ⌊n^θ⌋₊, θ > 0: for every δ > 0, eventually a_n / M_n ≤ n^(ρ - θ + δ).

theorem BGW.StableTrees.RegularlyVaryingSeq.tendsto_mul_div_floor_rpow {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 ≤ ρ) {η : ℝ} (hη : η < 1 - ρ) {l : Filter ℕ} (hl : l ≤ Filter.atTop) {e : ℕ → ℝ} (he0 : ∀ᶠ (n : ℕ) in l, 0 ≤ e n) (he : ∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in l, e n ≤ ↑n ^ δ) {ε : ℝ} (hε : 0 < ε) : Filter.Tendsto (fun (n : ℕ) => a n * e n / (ε * ↑⌊↑n ^ (1 - η)⌋₊)) l (nhds 0)

Lemma lem:critM (source lines 1090–1097): if η < 1 - ρ, ε > 0, and e_n ≥ 0 is n^{o(1)} along a filter l ≤ atTop, then a_n e_n / (ε ⌊n^(1-η)⌋₊) → 0 along l.

theorem BGW.StableTrees.RegularlyVaryingSeq.tendsto_div_floor_rpow {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 < ρ) {η : ℝ} (hη : η < 1) {l : Filter ℕ} (hl : l ≤ Filter.atTop) {e : ℕ → ℝ} (he0 : ∀ᶠ (n : ℕ) in l, 0 ≤ e n) (he : ∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in l, e n ≤ ↑n ^ δ) : Filter.Tendsto (fun (n : ℕ) => e n / a ⌊↑n ^ (1 - η)⌋₊) l (nhds 0)

Lemma lem:critM (source lines 1099–1105): if η < 1 and e_n ≥ 0 is n^{o(1)} along a filter l ≤ atTop, then e_n / a_{⌊n^(1-η)⌋} → 0 along l.