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.

References

• https://en.wikipedia.org/wiki/Abel%27s_summation_formula

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_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 : ℝ → 𝕜} (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.