English
A Nat-endpoint version of Abel's summation with the derivatives defined on the interval [n,m] for naturals n ≤ m, giving the same identity as in the real-endpoint statement but with floor-corrected endpoints.
Русский
Версия Абелловой суммы с натуральными концами: для n ≤ m в ℕ и дифференцируемости на [n,m] выполняется та же формула, что и в вещественном случае, but с использованием целочисленных этажей.
LaTeX
$$$\\sum_{k \\in Ioc n m} f(k) c(k) = f(m) \\left(\\sum_{k \\in Icc 0 m} c(k)\\right) - f(n) \\left(\\sum_{k \\in Icc 0 n} c(k)\\right) - \\int_{t \\in Ioc (n:ℝ) m} f'(t) \\sum_{k \\in Icc 0 ⌊t⌋_+} c(k) dt$$$
Lean4
/-- A version of `sum_mul_eq_sub_sub_integral_mul` where the endpoints are `Nat`. -/
theorem _root_.sum_mul_eq_sub_sub_integral_mul' {n m : ℕ} (h : n ≤ m)
(hf_diff : ∀ t ∈ Set.Icc (n : ℝ) m, DifferentiableAt ℝ f t) (hf_int : IntegrableOn (deriv f) (Set.Icc (n : ℝ) m)) :
∑ k ∈ Ioc n m, f k * c k =
f m * (∑ k ∈ Icc 0 m, c k) - f n * (∑ k ∈ Icc 0 n, c k) -
∫ t in Set.Ioc (n : ℝ) m, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k :=
by
convert sum_mul_eq_sub_sub_integral_mul c n.cast_nonneg (Nat.cast_le.mpr h) hf_diff hf_int
all_goals rw [Nat.floor_natCast]
