multipliable_one_add_of_summable_prod

English

If the sum ∑ f_i converges (to a) and the sum of all finite products converges, then the infinite product ∏ (1 + f_i) is multipliable.

Русский

Если сумма ∑ f_i сходится, то бесконечное произведение ∏ (1+ f_i) сходится как множитель.

LaTeX

$$$ \text{Summable } (f i) \rightarrow \text{Multipliable } (1 + f \cdot)$$$

Lean4

/-- `∏' i : ι, (1 + f i)` is convergent if `∑' s : Finset ι, ∏ i ∈ s, f i` is convergent.

For complete normed ring, see also `multipliable_one_add_of_summable`. -/
theorem multipliable_one_add_of_summable_prod (h : Summable (∏ i ∈ ·, f i)) : Multipliable (1 + f ·) :=
  by
  obtain ⟨a, h⟩ := h
  exact ⟨a, hasProd_one_add_of_hasSum_prod h⟩

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