Consequences of Abel summation for partial sums

Mathlib's Mathlib/NumberTheory/AbelSummation.lean proves the summation-by-parts identity ∑_{k ≤ x} f k c k = f x ∑_{k ≤ x} c k - ∫ f' (t) ∑_{k ≤ t} c k dt and derives convergence criteria from it. This file draws two further consequences from a growth hypothesis on the partial sums ∑_{1 ≤ k ≤ t} c k.

• A logarithmic weight. Mathlib's summable_mul_of_bigO_atTop' converts a bound on the partial sums of a sequence into the convergence of a weighted series, provided the weight is differentiable and the derivative of the weight against the partial sums admits an integrable majorant. This file performs that conversion once, for the weight (t (1 + log t) ^ 3)⁻¹ and partial sums growing like t log t. The weight is written with 1 + log t rather than log t so that it stays positive and smooth at t = 1, where Abel summation starts. Its derivative against an O(t log t) partial sum is O((t (1 + log t) ^ 2)⁻¹), which is integrable at infinity by comparison with Mathlib's log-Cauchy density integrableOn_Ioi_zero_inv_mul_one_add_log_sq.
• A power weight. If the partial sums grow like κ x, then the partial sums weighted by n ^ τ, for an exponent τ > -1, grow like κ x ^ (τ + 1) / (τ + 1). This is the step that moves a Tauberian conclusion for the coefficients a n n ^ (1 - σ) back to the coefficients a n.

Main declarations

• TauCeti.summable_div_mul_one_add_log_cube: if the partial sums ∑_{1 ≤ k ≤ t} u k of a nonnegative sequence are O(t log t), then ∑ u n / (n (1 + log n) ^ 3) converges.
• TauCeti.sum_Icc_rpow_mul_eq: the exact Abel-summation identity for the weight t ^ τ.
• TauCeti.tendsto_rpow_inv_mul_sum_Icc_rpow_mul: if x⁻¹ ∑_{1 ≤ n ≤ x} c n → κ, then (x ^ (τ + 1))⁻¹ ∑_{1 ≤ n ≤ x} n ^ τ c n → κ / (τ + 1) for τ > -1.

The comparison weight

The hypotheses of Abel summation

The weighted series

theorem TauCeti.summable_div_mul_one_add_log_cube {u : ℕ → ℝ} (hu : ∀ (n : ℕ), 0 ≤ u n) (hgrowth : (fun (t : ℝ) => ∑ k ∈ Finset.Icc 1 ⌊t⌋₊, u k) =O[Filter.atTop] fun (t : ℝ) => t * Real.log t) : Summable fun (n : ℕ) => u n / (↑n * (1 + Real.log ↑n) ^ 3)

Abel summation turns an O(t log t) growth bound into a convergent series. If the partial sums of a nonnegative sequence u satisfy ∑_{1 ≤ k ≤ t} u k = O(t log t), then ∑ u n / (n (1 + log n) ^ 3) converges: summation by parts against the weight (t (1 + log t) ^ 3)⁻¹ leaves the integrable majorant (t (1 + log t) ^ 2)⁻¹.

Partial sums against a power weight

theorem TauCeti.sum_Icc_rpow_mul_eq (c : ℕ → ℝ) (τ : ℝ) {x : ℝ} (hx : 1 ≤ x) : ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑n ^ τ * c n = x ^ τ * ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, c n - τ * ∫ (t : ℝ) in 1..x, t ^ (τ - 1) * ∑ n ∈ Finset.Icc 1 ⌊t⌋₊, c n

The Abel-summation identity sum_mul_eq_sub_integral_mul₀ for the weight t ^ τ: ∑_{1 ≤ n ≤ x} n ^ τ c n = x ^ τ S(x) - τ ∫ t in 1..x, t ^ (τ - 1) S(t) for x ≥ 1, where S(t) = ∑_{1 ≤ n ≤ t} c n.

theorem TauCeti.tendsto_rpow_inv_mul_sum_Icc_rpow_mul {c : ℕ → ℝ} {κ τ : ℝ} (hτ : -1 < τ) (h : Filter.Tendsto (fun (x : ℝ) => x⁻¹ * ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, c n) Filter.atTop (nhds κ)) : Filter.Tendsto (fun (x : ℝ) => (x ^ (τ + 1))⁻¹ * ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ↑n ^ τ * c n) Filter.atTop (nhds (κ / (τ + 1)))

Partial sums weighted by a power. If the partial sums of c grow like κ x, that is x⁻¹ ∑_{1 ≤ n ≤ x} c n → κ, then for every exponent τ > -1 the partial sums weighted by n ^ τ grow like κ x ^ (τ + 1) / (τ + 1): (x ^ (τ + 1))⁻¹ ∑_{1 ≤ n ≤ x} n ^ τ c n → κ / (τ + 1). No sign condition on c is needed.