English
A variant of Abel's summation with Nat endpoints: for m ∈ ℕ, the same equality holds with floors m cast to real and then rounded, reflecting the Nat-based endpoint version.
Русский
Вариант Абеллового суммирования сNat-концами: для m ∈ ℕ выполняется та же формула, приводимая к вещественным концам через округление.
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_integral_mul` where the endpoint is a `Nat`. -/
theorem sum_mul_eq_sub_integral_mul' (m : ℕ) (hf_diff : ∀ t ∈ Set.Icc (0 : ℝ) m, DifferentiableAt ℝ f t)
(hf_int : IntegrableOn (deriv f) (Set.Icc (0 : ℝ) m)) :
∑ k ∈ Icc 0 m, f k * c k =
f m * (∑ k ∈ Icc 0 m, c k) - ∫ t in Set.Ioc (0 : ℝ) m, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k :=
by
convert sum_mul_eq_sub_integral_mul c m.cast_nonneg hf_diff hf_int
all_goals rw [Nat.floor_natCast]
