multipliable_one_add_of_summable — Mathlib

English

If a real-valued function f has positive values eventually and ∑ log f_i converges, then ∏ f_i converges as well.

Русский

Если значения f(i) положительны eventually и ∑ log f_i сходится, то и ∏ f_i сходится.

LaTeX

$$$\prod_{i} f_i \text{ converges}$$$

Lean4

protected theorem multipliable_one_add_of_summable (hf : Summable f) : Multipliable (fun i ↦ 1 + f i) :=
  multipliable_of_summable_log (summable_log_one_add_of_summable hf)

Похожие утверждения