English
If ∑ ‖f‖ converges and g tends to a finite limit c along cofinite filter, then ∑ ‖f(n) · g(n)‖ converges.
Русский
Если сумма по i от ‖f(i)‖ сходится и g(n) стремится к конечному пределу c по фильтру cofinite, то сумма по i от ‖f(i) g(i)‖ сходится.
LaTeX
$$$ \\text{Summable }(\\|f\\|) \\ \\wedge\\ \\text{Tendsto } g \\ cof (\\mathcal{N} c) \\Rightarrow \\text{Summable } (\\|f \\cdot g\\|) $$$
Lean4
theorem mul_tendsto_const {F ι : Type*} [NormedRing F] [NormMulClass F] [NormOneClass F] [CompleteSpace F] {f g : ι → F}
(hf : Summable fun n ↦ ‖f n‖) {c : F} (hg : Tendsto g cofinite (𝓝 c)) : Summable fun n ↦ f n * g n :=
by
apply summable_of_isBigO hf
simpa using (isBigO_const_mul_self 1 f _).mul (hg.isBigO_one F)
