English
Nat-endpoint variant of the previous Nat-based Abel identity; the statement mirrors with floors and real endpoints cast to Nat.
Русский
Натурально-конечная версия идентичности Абеля; утверждение аналогично предыдущим, но с округлениями кNat。
LaTeX
$$$\\sum_{k \\in Ioc 0 m} f(k) c(k) = f(m) \\sum_{k \\in Icc 0 m} c(k) - \\int_{t \\in Ioc 0 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₀' (hc : c 0 = 0) (m : ℕ) (hf_diff : ∀ t ∈ Set.Icc (1 : ℝ) m, DifferentiableAt ℝ f t)
(hf_int : IntegrableOn (deriv f) (Set.Icc (1 : ℝ) m)) :
∑ k ∈ Icc 0 m, f k * c k =
f m * (∑ k ∈ Icc 0 m, c k) - ∫ t in Set.Ioc (1 : ℝ) m, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k :=
by
convert sum_mul_eq_sub_integral_mul₀ c hc m hf_diff hf_int
all_goals rw [Nat.floor_natCast]
