feat(Topology/InfiniteSum): tprod_one_{add/sub}_ordered

Author: wwylele

Mathlib/Algebra/BigOperators/Ring/Finset.lean

@@ -220,6 +220,11 @@ theorem prod_add_ordered [LinearOrder ι] (s : Finset ι) (f g : ι → R) :
       mul_left_comm]
     exact mt (fun ha => (mem_filter.1 ha).1) ha'
 
+theorem prod_one_add_ordered [LinearOrder ι] (s : Finset ι) (f : ι → R) :
+    ∏ i ∈ s, (1 + f i) = 1 + ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 + f j) := by
+  rw [prod_add_ordered]
+  simp
+
 /-- Summing `a ^ #t * b ^ (n - #t)` over all finite subsets `t` of a finset `s`
 gives `(a + b) ^ #s`. -/
 theorem sum_pow_mul_eq_add_pow (a b : R) (s : Finset ι) :

Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

@@ -307,4 +307,43 @@ 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
 
+section Ordered
+variable [LinearOrder ι] [LocallyFiniteOrderBot ι] [T2Space α]
+
+/-- The infinite version of `Finset.prod_one_add_ordered`. -/
+theorem tprod_one_add_ordered [ContinuousAdd α]
+    (hsum : Summable fun i ↦ f i * ∏ j ∈ Iio i, (1 + f j))
+    (hprod : Multipliable (1 + f ·)) :
+    ∏' i, (1 + f i) = 1 + ∑' i, f i * ∏ j ∈ Iio i, (1 + f j) := by
+  rcases isEmpty_or_nonempty ι with _ | _
+  · simp
+  obtain ⟨x, hx⟩ := hprod
+  obtain ⟨a, ha⟩ := hsum
+  convert hx.tprod_eq
+  unfold HasProd at hx
+  conv at hx in fun _ ↦ _ => ext _; rw [prod_one_add_ordered] -- simp_rw would cause loop
+  rw [ha.tsum_eq]
+  refine (tendsto_nhds_unique (hx.comp tendsto_finset_Iic_atTop_atTop) ?_).symm
+  apply Tendsto.const_add
+  convert ha.comp tendsto_finset_Iic_atTop_atTop using 2 with s
+  refine sum_congr rfl (fun i hi ↦ ?_)
+  congr
+  ext j
+  suffices j < i → j ≤ s by simpa
+  exact fun hj ↦ (hj.trans_le (by simpa using hi)).le
+
+omit [CommSemiring α] in
+/-- The infinite version of `Finset.prod_one_sub_ordered`. -/
+theorem tprod_one_sub_ordered [CommRing α] [IsTopologicalAddGroup α]
+    (hsum : Summable fun i ↦ f i * ∏ j ∈ Iio i, (1 - f j))
+    (hprod : Multipliable (1 - f ·)) :
+    ∏' i, (1 - f i) = 1 - ∑' i, f i * ∏ j ∈ Iio i, (1 - f j) := by
+  simp_rw [sub_eq_add_neg] at hsum hprod ⊢
+  obtain hsum' := hsum.neg
+  simp_rw [← neg_mul] at hsum'
+  simp_rw [← tsum_neg, ← neg_mul]
+  exact tprod_one_add_ordered hsum' hprod
+
+end Ordered
+
 end ProdOneSum