Linear growth of partial sums from a window bound

If nonnegative terms f n have sums over the multiplicative windows q x < n ≤ x bounded by a multiple of x, for a fixed ratio 0 ≤ q < 1 and all large x, then their partial sums ∑_{1 ≤ n ≤ x} f n are O(x): the partial sum up to x is the window sum plus the partial sum up to q x, and the window bounds form a geometric series.

This is the summation step of Chebyshev-type bounds, where a local estimate on windows (q x, x] comes from a smoothed average and the global linear bound is what is needed.

Main results

• TauCeti.isBigO_sum_Icc_of_sum_Ioc_floor_mul_le: a window bound O(x) implies partial sums O(x).
• TauCeti.exists_sum_Icc_le_mul_of_isBigO: partial sums that are O(x) are bounded by C N at every natural cutoff N, with one constant C.

theorem TauCeti.isBigO_sum_Icc_of_sum_Ioc_floor_mul_le {f : ℕ → ℝ} (hf : 0 ≤ f) {q K : ℝ} (hq0 : 0 ≤ q) (hq1 : q < 1) (h : ∀ᶠ (x : ℝ) in Filter.atTop, ∑ n ∈ Finset.Ioc ⌊q * x⌋₊ ⌊x⌋₊, f n ≤ K * x) : (fun (x : ℝ) => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, f n) =O[Filter.atTop] fun (x : ℝ) => x

Summing windows. If nonnegative terms f n have sums over the windows q x < n ≤ x bounded by K x for all large x, where 0 ≤ q < 1 is a fixed ratio, then their partial sums ∑_{1 ≤ n ≤ x} f n are O(x).

theorem TauCeti.exists_sum_Icc_le_mul_of_isBigO {f : ℕ → ℝ} (h : (fun (x : ℝ) => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, f n) =O[Filter.atTop] fun (x : ℝ) => x) : ∃ (C : ℝ), ∀ (N : ℕ), ∑ n ∈ Finset.Icc 1 N, f n ≤ C * ↑N

A uniform linear bound from linear growth. If the partial sums ∑_{1 ≤ n ≤ x} f n are O(x), then a single constant C bounds them by C N at every natural cutoff N, including the finitely many cutoffs below the range where the O(x) estimate starts.