English
Abel's summation specialized when the first coefficient c(0) = 0; under a simple nontrivial interval, the equality reduces with c0 eliminated.
Русский
Абеллова сумма при условии c(0) = 0: формула упрощается, так как нулевой член не вносит вклад.
LaTeX
$$$\\sum_{k \\in Icc 0 ⌊b⌋_+} f(k) c(k) = f(b) \\left(\\sum_{k \\in Icc 0 ⌊b⌋_+} c(k)\\right) - \\int_{t \\in Ioc 1 b} f'(t) \\sum_{k \\in Icc 0 ⌊t⌋_+} c(k) dt$$$
Lean4
/-- Specialized version of `sum_mul_eq_sub_integral_mul` when the first coefficient of the sequence
`c` is equal to `0`. -/
theorem sum_mul_eq_sub_integral_mul₀ (hc : c 0 = 0) (b : ℝ) (hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t)
(hf_int : IntegrableOn (deriv f) (Set.Icc 1 b)) :
∑ k ∈ Icc 0 ⌊b⌋₊, f k * c k =
f b * (∑ k ∈ Icc 0 ⌊b⌋₊, c k) - ∫ t in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k :=
by
obtain hb | hb := le_or_gt 1 b
· have : 1 ≤ ⌊b⌋₊ := (Nat.one_le_floor_iff _).mpr hb
nth_rewrite 1 [Icc_eq_cons_Ioc (Nat.zero_le _), sum_cons, ← Icc_add_one_left_eq_Ioc, Icc_eq_cons_Ioc (by cutsat),
sum_cons]
rw [zero_add, ← Nat.floor_one (R := ℝ), sum_mul_eq_sub_sub_integral_mul c zero_le_one hb hf_diff hf_int,
Nat.floor_one, Nat.cast_one, Icc_eq_cons_Ioc zero_le_one, sum_cons, show 1 = 0 + 1 by rfl, Nat.Ioc_succ_singleton,
zero_add, sum_singleton, hc, mul_zero, zero_add]
ring
·
simp_rw [Nat.floor_eq_zero.mpr hb, Icc_self, sum_singleton, Nat.cast_zero, hc, mul_zero,
Set.Ioc_eq_empty_of_le hb.le, Measure.restrict_empty, integral_zero_measure, sub_self]
