multipliable_of_summable_log — Mathlib

English

If log f_i converges (i.e., has a finite sum) and every f_i ≠ 0, then the infinite product ∏ f_i exists (converges).

Русский

Если сумма log f_i сходится и все f_i ≠ 0, то бесконечное произведение ∏ f_i существует (сходится).

LaTeX

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

Lean4

theorem multipliable_of_summable_log (hf : Summable fun i ↦ log (f i)) : Multipliable f :=
  by
  by_cases hfn : ∃ n, f n = 0
  · exact multipliable_of_exists_eq_zero hfn
  · exact ⟨_, hasProd_of_hasSum_log (not_exists.mp hfn) hf.hasSum⟩

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