English
A Nat-endpoint version of Abel's summation: for n ≤ m in ℕ and suitable differentiability/integrability hypotheses, the finite sum ∑_{k=n+1}^{m} f(k)c(k) equals the boundary terms at m and n minus the integral of f' times a companion partial sum.
Русский
Версия Абеллевой суммы с концами в натуральных числах: для натуральных n ≤ m и подходящих условий дифференцируемости/интегрируемости выполняется тождество для конечной суммы ∑_{k=n+1}^{m} f(k)c(k) с соответствующими границами и интегралом.
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 \\lfloor t \\rfloor_+} c(k) \\, dt$$$
Lean4
/-- Abel's summation formula. -/
theorem _root_.sum_mul_eq_sub_sub_integral_mul (ha : 0 ≤ a) (hab : a ≤ b)
(hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) (hf_int : IntegrableOn (deriv f) (Set.Icc a b)) :
∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f k * c k =
f b * (∑ k ∈ Icc 0 ⌊b⌋₊, c k) - f a * (∑ k ∈ Icc 0 ⌊a⌋₊, c k) -
∫ t in Set.Ioc a b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k :=
by
rw [← integral_of_le hab]
have aux1 : ⌊a⌋₊ ≤ a := Nat.floor_le ha
have aux2 : b ≤ ⌊b⌋₊ + 1 := (Nat.lt_floor_add_one _).le
obtain hb | hb := eq_or_lt_of_le (Nat.floor_le_floor hab)
·
rw [hb, Ioc_eq_empty_of_le le_rfl, sum_empty, ← sub_mul,
integralmulsum c hf_diff hf_int _ _ ⌊b⌋₊ hab (hb ▸ aux1) aux2 le_rfl le_rfl, sub_self]
have aux3 : a ≤ ⌊a⌋₊ + 1 := (Nat.lt_floor_add_one _).le
have aux4 : ⌊a⌋₊ + 1 ≤ b := by rwa [← Nat.cast_add_one, ← Nat.le_floor_iff (ha.trans hab)]
have aux5 : ⌊b⌋₊ ≤ b := Nat.floor_le (ha.trans hab)
have aux6 : a ≤ ⌊b⌋₊ := Nat.floor_lt ha |>.mp hb |>.le
simp_rw [← smul_eq_mul, sum_Ioc_by_parts (fun k ↦ f k) _ hb, range_eq_Ico, Ico_add_one_right_eq_Icc, smul_eq_mul]
have :
∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(k + 1) - f k) * ∑ n ∈ Icc 0 k, c n =
∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ t in k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n :=
by
rw [← Ico_add_one_add_one_eq_Ioc, Nat.sub_add_cancel (by cutsat), Eq.comm]
exact
sum_congr rfl fun k hk ↦
(integralmulsum c hf_diff hf_int _ _ _ (mod_cast k.le_succ) le_rfl (mod_cast le_rfl) (ineqofmemIco' hk).1 <|
mod_cast (ineqofmemIco' hk).2)
rw [this, sum_integral_adjacent_intervals_Ico hb, Nat.cast_add, Nat.cast_one, ←
integral_interval_sub_left (a := a) (c := ⌊a⌋₊ + 1), ← integral_add_adjacent_intervals (b := ⌊b⌋₊) (c := b),
integralmulsum c hf_diff hf_int _ _ _ aux3 aux1 le_rfl le_rfl aux4,
integralmulsum c hf_diff hf_int _ _ _ aux5 le_rfl aux2 aux6 le_rfl]
·
ring
-- now deal with the integrability side goals
-- (Note we have 5 goals, but the 1st and 3rd are identical. TODO: find a non-hacky way of dealing
-- with both at once.)
· rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux6]
exact (integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_right aux5)
· rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux5]
exact (integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_left aux6)
· rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux6]
exact (integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_right aux5)
· rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux3]
exact (integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_right aux4)
·
exact fun k hk ↦
(intervalIntegrable_iff_integrableOn_Icc_of_le (mod_cast k.le_succ)).mpr <|
(integrableOn_mul_sum_Icc c ha hf_int).mono_set <|
(Set.Icc_subset_Icc_iff (mod_cast k.le_succ)).mpr <| mod_cast (ineqofmemIco hk)
