English
If the growth of |f| and the cumulative sums are controlled by a Big-O bound relative to 1 at infinity, then the weighted sum ∑ f(n)c(n) is summable.
Русский
Если величины |f| и суммарные кумулятивные суммы контролируются по Big-O относительно константы на бесконечности, то сумма weighted ∑ f(n)c(n) сходится.
LaTeX
$$$\\sum_{n} f(n)c(n) \\text{ is Summable under } |f(n)|n = O(1) \\text{ at } \\infty$$$
Lean4
theorem summable_mul_of_bigO_atTop (hf_diff : ∀ t ∈ Set.Ici 0, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t)
(hf_int : LocallyIntegrableOn (deriv (fun t ↦ ‖f t‖)) (Set.Ici 0))
(h_bdd : (fun n : ℕ ↦ ‖f n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun _ ↦ (1 : ℝ)) {g : ℝ → ℝ}
(hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g) (hg₂ : IntegrableAtFilter g atTop) :
Summable (fun n : ℕ ↦ f n * c n) :=
by
refine summable_mul_of_bigO_atTop_aux c 0 h_bdd (by rwa [Nat.cast_zero]) (fun n ↦ ?_) hg₁ hg₂
exact_mod_cast
sum_mul_eq_sub_integral_mul' _ _ (fun _ ht ↦ hf_diff _ ht.1)
(hf_int.integrableOn_compact_subset Set.Icc_subset_Ici_self isCompact_Icc)
