Abel's summation formula #

We prove several versions of Abel's summation formula.

Results #

sum_mul_eq_sub_sub_integral_mul: general statement of the formula for a sum between two (nonnegative) reals a and b.
sum_mul_eq_sub_integral_mul: a specialized version of sum_mul_eq_sub_sub_integral_mul for the case a = 0.
sum_mul_eq_sub_integral_mul₀: a specialized version of sum_mul_eq_sub_integral_mul for when the first coefficient of the sequence is 0. This is useful for ArithmeticFunction.

Primed versions of the three results above are also stated for when the endpoints are Nat.

tendsto_sum_mul_atTop_nhds_one_sub_integral: limit version of sum_mul_eq_sub_integral_mul when a tends to ∞.
tendsto_sum_mul_atTop_nhds_one_sub_integral₀: limit version of sum_mul_eq_sub_integral_mul₀ when a tends to ∞.
summable_mul_of_bigO_atTop: let c : ℕ → 𝕜 and f : ℝ → 𝕜 with 𝕜 = ℝ or ℂ, prove the summability of n ↦ (c n) * (f n) using Abel's formula under some bigO assumptions at infinity.

theorem sum_mul_eq_sub_sub_integral_mul {𝕜 : Type u_1} [RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) (hf_int : MeasureTheory.IntegrableOn (deriv f) (Set.Icc a b) MeasureTheory.volume) :

∑ k ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊, f ↑k * c k = f b * ∑ k ∈ Finset.Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Finset.Icc 0 ⌊a⌋₊, c k - ∫ (t : ℝ) in Set.Ioc a b, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k

Abel's summation formula.

theorem sum_mul_eq_sub_sub_integral_mul' {𝕜 : Type u_1} [RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} {n m : ℕ} (h : n ≤ m) (hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t) (hf_int : MeasureTheory.IntegrableOn (deriv f) (Set.Icc ↑n ↑m) MeasureTheory.volume) :

∑ k ∈ Finset.Ioc n m, f ↑k * c k = f ↑m * ∑ k ∈ Finset.Icc 0 m, c k - f ↑n * ∑ k ∈ Finset.Icc 0 n, c k - ∫ (t : ℝ) in Set.Ioc ↑n ↑m, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k

A version of sum_mul_eq_sub_sub_integral_mul where the endpoints are Nat.

theorem sum_mul_eq_sub_integral_mul {𝕜 : Type u_1} [RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} {b : ℝ} (hb : 0 ≤ b) (hf_diff : ∀ t ∈ Set.Icc 0 b, DifferentiableAt ℝ f t) (hf_int : MeasureTheory.IntegrableOn (deriv f) (Set.Icc 0 b) MeasureTheory.volume) :

∑ k ∈ Finset.Icc 0 ⌊b⌋₊, f ↑k * c k = f b * ∑ k ∈ Finset.Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 0 b, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k

Specialized version of sum_mul_eq_sub_sub_integral_mul for the case a = 0.

theorem sum_mul_eq_sub_integral_mul' {𝕜 : Type u_1} [RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} (m : ℕ) (hf_diff : ∀ t ∈ Set.Icc 0 ↑m, DifferentiableAt ℝ f t) (hf_int : MeasureTheory.IntegrableOn (deriv f) (Set.Icc 0 ↑m) MeasureTheory.volume) :

∑ k ∈ Finset.Icc 0 m, f ↑k * c k = f ↑m * ∑ k ∈ Finset.Icc 0 m, c k - ∫ (t : ℝ) in Set.Ioc 0 ↑m, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k

A version of sum_mul_eq_sub_integral_mul where the endpoint is a Nat.

theorem sum_mul_eq_sub_integral_mul₀ {𝕜 : Type u_1} [RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} (hc : c 0 = 0) (b : ℝ) (hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t) (hf_int : MeasureTheory.IntegrableOn (deriv f) (Set.Icc 1 b) MeasureTheory.volume) :

∑ k ∈ Finset.Icc 0 ⌊b⌋₊, f ↑k * c k = f b * ∑ k ∈ Finset.Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k

Specialized version of sum_mul_eq_sub_integral_mul when the first coefficient of the sequence c is equal to 0.

theorem sum_mul_eq_sub_integral_mul₀' {𝕜 : Type u_1} [RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} (hc : c 0 = 0) (m : ℕ) (hf_diff : ∀ t ∈ Set.Icc 1 ↑m, DifferentiableAt ℝ f t) (hf_int : MeasureTheory.IntegrableOn (deriv f) (Set.Icc 1 ↑m) MeasureTheory.volume) :

∑ k ∈ Finset.Icc 0 m, f ↑k * c k = f ↑m * ∑ k ∈ Finset.Icc 0 m, c k - ∫ (t : ℝ) in Set.Ioc 1 ↑m, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k

A version of sum_mul_eq_sub_integral_mul₀ where the endpoint is a Nat.

Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.Icc 0 n, f ↑k * c k) Filter.atTop (nhds (l - ∫ (t : ℝ) in Set.Ioi 0, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k))

Filter.Tendsto (fun (n : ℕ) => ∑ k ∈ Finset.Icc 0 n, f ↑k * c k) Filter.atTop (nhds (l - ∫ (t : ℝ) in Set.Ioi 1, deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k))

theorem summable_mul_of_bigO_atTop {𝕜 : Type u_1} [RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} (hf_diff : ∀ t ∈ Set.Ici 0, DifferentiableAt ℝ (fun (x : ℝ) => ‖f x‖) t) (hf_int : MeasureTheory.IntegrableOn (deriv fun (t : ℝ) => ‖f t‖) (Set.Ici 0) MeasureTheory.volume) (h_bdd : (fun (n : ℕ) => ‖f ↑n‖ * ∑ k ∈ Finset.Icc 0 n, ‖c k‖) =O[Filter.atTop ] fun (x : ℕ) => 1) {g : ℝ → ℝ} (hg₁ : (fun (t : ℝ) => deriv (fun (t : ℝ) => ‖f t‖) t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, ‖c k‖) =O[Filter.atTop ] g) (hg₂ : MeasureTheory.IntegrableAtFilter g Filter.atTop MeasureTheory.volume) :

Summable fun (n : ℕ) => f ↑n * c n

theorem summable_mul_of_bigO_atTop' {𝕜 : Type u_1} [RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} (hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun (x : ℝ) => ‖f x‖) t) (hf_int : MeasureTheory.IntegrableOn (deriv fun (t : ℝ) => ‖f t‖) (Set.Ici 1) MeasureTheory.volume) (h_bdd : (fun (n : ℕ) => ‖f ↑n‖ * ∑ k ∈ Finset.Icc 1 n, ‖c k‖) =O[Filter.atTop ] fun (x : ℕ) => 1) {g : ℝ → ℝ} (hg₁ : (fun (t : ℝ) => deriv (fun (t : ℝ) => ‖f t‖) t * ∑ k ∈ Finset.Icc 1 ⌊t⌋₊, ‖c k‖) =O[Filter.atTop ] g) (hg₂ : MeasureTheory.IntegrableAtFilter g Filter.atTop MeasureTheory.volume) :

Summable fun (n : ℕ) => f ↑n * c n

A version of summable_mul_of_bigO_atTop that can be useful to avoid difficulties near zero.