Theorems · Theorem · number theory

sum_mul_eq_sub_sub_integral_mul

∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (c : ℕ → 𝕜) {f : ℝ → 𝕜} {a b : ℝ},
  0 ≤ a →
    a ≤ b →
      (∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) →
        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.

Defined in

Mathlib.NumberTheory.AbelSummation

Cited by

4 results in Mathlib

Foundations

Depth 270 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLike