Karamata-type sums for regularly varying sequences

Source lines 1141–1148 and 1173–1179 (inventory B12): for a monotone sequence a, positive at n ≥ 1, regularly varying of index ρ:

• RegularlyVaryingSeq.karamata_tail (ρ > 0): ∑_{m < q ≤ N} 1 / (q a_q) ≤ C / a_m for all 1 ≤ m and all N, with one constant C; RegularlyVaryingSeq.summable_inv_mul and RegularlyVaryingSeq.karamata_tail_tsum give summability and the bound for the full tail ∑_{q > m} (a tsum of an indicator).
• RegularlyVaryingSeq.karamata_sum (0 ≤ ρ < 1): ∑_{h=1}^{n} 1 / a_h ≤ C n / a_n for all n.

The source invokes "Karamata's theorem". Here the bounds follow from the global Potter bounds (RegularlyVaryingSeq.exists_potter_global) by comparison with the power sums ∑_{q > m} q^{-1-s} ≤ m^{-s}/s and ∑_{h ≤ n} h^{-s} ≤ n^{1-s}/(1-s), which are proved by telescoping.

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

theorem BGW.StableTrees.rpow_neg_sub_rpow_neg_ge {y z s : ℝ} (hy : 0 < y) (hyz : y ≤ z) (hs : 0 ≤ s) : s * (z - y) * z ^ (-s - 1) ≤ y ^ (-s) - z ^ (-s)

Telescoping bound for negative powers: for 0 < y ≤ z and s ≥ 0, s (z - y) z^(-s-1) ≤ y^(-s) - z^(-s).

theorem BGW.StableTrees.rpow_sub_rpow_ge {y z p : ℝ} (hy : 0 ≤ y) (hyz : y ≤ z) (hz : 0 < z) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : p * (z - y) * z ^ (p - 1) ≤ z ^ p - y ^ p

Telescoping bound for powers in [0,1]: for 0 ≤ y ≤ z, 0 < z and 0 ≤ p ≤ 1, p (z - y) z^(p-1) ≤ z^p - y^p.

theorem BGW.StableTrees.sum_Ioc_rpow_neg_le {s : ℝ} (hs : 0 < s) {m : ℕ} (hm : 1 ≤ m) (N : ℕ) : ∑ q ∈ Finset.Ioc m N, ↑q ^ (-s - 1) ≤ ↑m ^ (-s) / s

∑_{m < q ≤ N} q^(-s-1) ≤ m^(-s) / s for s > 0, m ≥ 1.

theorem BGW.StableTrees.sum_Icc_rpow_neg_le {s : ℝ} (hs0 : 0 ≤ s) (hs1 : s < 1) (n : ℕ) : ∑ h ∈ Finset.Icc 1 n, ↑h ^ (-s) ≤ ↑n ^ (1 - s) / (1 - s)

∑_{h=1}^{n} h^(-s) ≤ n^(1-s) / (1-s) for 0 ≤ s < 1.

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

Termwise comparison behind the Karamata tail bound: with s = ρ/2, there is C > 0 with 1 / (q a_q) ≤ (C m^s / a_m) q^(-s-1) for all 1 ≤ m ≤ q.

theorem BGW.StableTrees.RegularlyVaryingSeq.summable_inv_mul {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 < ρ) : Summable fun (q : ℕ) => 1 / (↑q * a q)

The series ∑_q 1 / (q a_q) converges (positive index).

theorem BGW.StableTrees.RegularlyVaryingSeq.karamata_tail {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 < ρ) : ∃ (C : ℝ), 0 < C ∧ ∀ (m N : ℕ), 1 ≤ m → ∑ q ∈ Finset.Ioc m N, 1 / (↑q * a q) ≤ C / a m

Karamata tail bound (source lines 1141–1148): for ρ > 0 there is C > 0 such that for all m ≥ 1 and all N, ∑_{m < q ≤ N} 1 / (q a_q) ≤ C / a_m.

theorem BGW.StableTrees.RegularlyVaryingSeq.karamata_tail_tsum {ρ : ℝ} {a : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ a) (hmono : Monotone a) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < a n) (hρ : 0 < ρ) : ∃ (C : ℝ), 0 < C ∧ ∀ (m : ℕ), 1 ≤ m → ∑' (q : ℕ), (Set.Ioi m).indicator (fun (q : ℕ) => 1 / (↑q * a q)) q ≤ C / a m

Karamata tail bound, full-tail form: for ρ > 0 there is C > 0 such that for all m ≥ 1, ∑_{q > m} 1 / (q a_q) ≤ C / a_m (the series being summable, see summable_inv_mul).

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

Karamata partial-sum bound (source lines 1173–1179): for 0 ≤ ρ < 1 there is C > 0 such that for all n, ∑_{h=1}^{n} 1 / a_h ≤ C n / a_n.