feat(Topology/InfiniteSum): Formula for ∏' i : ι, (1 + f i) (#29857)

This is the infinite version of [Finset.prod_one_add](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Ring/Finset.html#Finset.prod_one_add). Unfortunately I think it only holds in the Summable->Multipliable direction, but not the opposite way. 

One usage of this is in generating power series of partition functions (infinite version of those in https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/Partition.lean). Using these lemma one can quickly argue about general multipliability,  and direct calculation if the product factor is `(1 + monomial)`

Author: wwylele

Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import Mathlib.Algebra.BigOperators.NatAntidiagonal
+import Mathlib.Algebra.BigOperators.Ring.Finset
 import Mathlib.Topology.Algebra.InfiniteSum.Constructions
 import Mathlib.Topology.Algebra.Ring.Basic
 
@@ -15,6 +16,7 @@ This file provides lemmas about the interaction between infinite sums and multip
 ## Main results
 
 * `tsum_mul_tsum_eq_tsum_sum_antidiagonal`: Cauchy product formula
+* `tprod_one_add`: expanding `∏' i : ι, (1 + f i)` as infinite sum.
 -/
 
 open Filter Finset Function
@@ -251,3 +253,33 @@ protected theorem Summable.tsum_mul_tsum_eq_tsum_sum_range (hf : Summable f) (hg
 end Nat
 
 end CauchyProduct
+
+section ProdOneSum
+
+/-!
+### Infinite product of `1 + f i`
+
+This section extends `Finset.prod_one_add` to the infinite product
+`∏' i : ι, (1 + f i) = ∑' s : Finset ι, ∏ i ∈ s, f i`.
+-/
+
+variable [CommSemiring α] [TopologicalSpace α] {f : ι → α}
+
+theorem hasProd_one_add_of_hasSum_prod {a : α} (h : HasSum (∏ i ∈ ·, f i) a) :
+    HasProd (1 + f ·) a := by
+  simp_rw [HasProd, prod_one_add]
+  exact h.comp tendsto_finset_powerset_atTop_atTop
+
+/-- `∏' 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⟩
+
+theorem tprod_one_add [T2Space α] (h : Summable (∏ i ∈ ·, f i)) :
+    ∏' i, (1 + f i) = ∑' s, ∏ i ∈ s, f i :=
+  HasProd.tprod_eq <| hasProd_one_add_of_hasSum_prod h.hasSum
+
+end ProdOneSum