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.

References

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

theorem integrableOn_mul_sum_Icc {𝕜 : Type u_1} [RCLike 𝕜] (c : ℕ → 𝕜) {a b : ℝ} {m : ℕ} (ha : 0 ≤ a) {g : ℝ → 𝕜} (hg_int : MeasureTheory.IntegrableOn g (Set.Icc a b) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (t : ℝ) => g t * ∑ k ∈ Finset.Icc m ⌊t⌋₊, c k) (Set.Icc a b) MeasureTheory.volume

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.

theorem locallyIntegrableOn_mul_sum_Icc {𝕜 : Type u_1} [RCLike 𝕜] (c : ℕ → 𝕜) {a : ℝ} {m : ℕ} (ha : 0 ≤ a) {g : ℝ → 𝕜} (hg : MeasureTheory.LocallyIntegrableOn g (Set.Ici a) MeasureTheory.volume) : MeasureTheory.LocallyIntegrableOn (fun (t : ℝ) => g t * ∑ k ∈ Finset.Icc m ⌊t⌋₊, c k) (Set.Ici a) MeasureTheory.volume

theorem tendsto_sum_mul_atTop_nhds_one_sub_integral {𝕜 : Type u_1} [RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} (hf_diff : ∀ t ∈ Set.Ici 0, DifferentiableAt ℝ f t) (hf_int : MeasureTheory.LocallyIntegrableOn (deriv f) (Set.Ici 0) MeasureTheory.volume) {l : 𝕜} (h_lim : Filter.Tendsto (fun (n : ℕ) => f ↑n * ∑ k ∈ Finset.Icc 0 n, c k) Filter.atTop (nhds l)) {g : ℝ → 𝕜} (hg_dom : (fun (t : ℝ) => deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k) =O[Filter.atTop] g) (hg_int : MeasureTheory.IntegrableAtFilter g Filter.atTop MeasureTheory.volume) : 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))

theorem tendsto_sum_mul_atTop_nhds_one_sub_integral₀ {𝕜 : Type u_1} [RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} (hc : c 0 = 0) (hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t) (hf_int : MeasureTheory.LocallyIntegrableOn (deriv f) (Set.Ici 1) MeasureTheory.volume) {l : 𝕜} (h_lim : Filter.Tendsto (fun (n : ℕ) => f ↑n * ∑ k ∈ Finset.Icc 0 n, c k) Filter.atTop (nhds l)) {g : ℝ → ℝ} (hg_dom : (fun (t : ℝ) => deriv f t * ∑ k ∈ Finset.Icc 0 ⌊t⌋₊, c k) =O[Filter.atTop] g) (hg_int : MeasureTheory.IntegrableAtFilter g Filter.atTop MeasureTheory.volume) : 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.LocallyIntegrableOn (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.LocallyIntegrableOn (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.