English
A specialized Abel summation for the case a = 0: under suitable differentiability/integrability assumptions, the sum ∑_{k=0}^{⌊b⌋} f(k)c(k) equals f(b)∑_{k=0}^{⌊b⌋} c(k) minus the integral of f' times the cumulative sum of c up to ⌊t⌋ over t in (0,b].
Русский
Специализированное суммирование Абеля в случае a=0: при подходящих условиях дифференцируемости и интегрируемости имеет место тождество для суммы от 0 до ⌊b⌋.
LaTeX
$$$\\sum_{k \\in Icc 0 ⌊b⌋_+} f(k) c(k) = f(b)\\sum_{k \\in Icc 0 ⌊b⌋_+} c(k) - \\int_{t \\in Ioc 0 b} f'(t) \\sum_{k \\in Icc 0 ⌊t⌋_+} c(k) \\, dt$$$
Lean4
/-- Specialized version of `sum_mul_eq_sub_sub_integral_mul` for the case `a = 0` -/
theorem sum_mul_eq_sub_integral_mul {b : ℝ} (hb : 0 ≤ b) (hf_diff : ∀ t ∈ Set.Icc 0 b, DifferentiableAt ℝ f t)
(hf_int : IntegrableOn (deriv f) (Set.Icc 0 b)) :
∑ k ∈ Icc 0 ⌊b⌋₊, f k * c k =
f b * (∑ k ∈ Icc 0 ⌊b⌋₊, c k) - ∫ t in Set.Ioc 0 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k :=
by
nth_rewrite 1 [Icc_eq_cons_Ioc (Nat.zero_le _)]
rw [sum_cons, ← Nat.floor_zero (R := ℝ), sum_mul_eq_sub_sub_integral_mul c le_rfl hb hf_diff hf_int, Nat.floor_zero,
Nat.cast_zero, Icc_self, sum_singleton]
ring
