English
Under differentiability and local integrability conditions, the weighted sums defined by Abel’s method are summable if the derivative of f is integrable on the interval in question.
Русский
При дифференцируемости и локальной интегрируемости производной f взвешенные суммы Абеля сходятся при заданном интервале.
LaTeX
$$$\\text{Summable}(\\, f(n)c(n) \\HEQ) \\text{ if } \\int (deriv f) S(t) dt < \\infty$$$
Lean4
/-- A version of `summable_mul_of_bigO_atTop` that can be useful to avoid difficulties near zero. -/
theorem summable_mul_of_bigO_atTop' (hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t)
(hf_int : LocallyIntegrableOn (deriv (fun t ↦ ‖f t‖)) (Set.Ici 1))
(h_bdd : (fun n : ℕ ↦ ‖f n‖ * ∑ k ∈ Icc 1 n, ‖c k‖) =O[atTop] fun _ ↦ (1 : ℝ)) {g : ℝ → ℝ}
(hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖) =O[atTop] g) (hg₂ : IntegrableAtFilter g atTop) :
Summable (fun n : ℕ ↦ f n * c n) :=
by
have h : ∀ n, ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n ↦ if n = 0 then 0 else c n) k‖ :=
by
intro n
rw [Icc_eq_cons_Ioc n.zero_le, sum_cons, ← Icc_add_one_left_eq_Ioc, zero_add]
simp_rw [if_pos, norm_zero, zero_add]
exact Finset.sum_congr rfl fun _ h ↦ by rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp h).1).ne']
simp_rw [h] at h_bdd hg₁
refine
Summable.congr_atTop
(summable_mul_of_bigO_atTop_aux (fun n ↦ if n = 0 then 0 else c n) 1 h_bdd (by rwa [Nat.cast_one]) (fun n ↦ ?_)
hg₁ hg₂)
?_
·
exact_mod_cast
sum_mul_eq_sub_integral_mul₀' _ (by simp only [reduceIte, norm_zero]) n (fun _ ht ↦ hf_diff _ ht.1)
(hf_int.integrableOn_compact_subset Set.Icc_subset_Ici_self isCompact_Icc)
· filter_upwards [eventually_ne_atTop 0] with k hk
simp_rw [if_neg hk]
