feat: Infinite products (#11733)

Last year, YaelDillies made a pull request to mathlib3 that unfortunately never got merged in: leanprover-community/mathlib#18405. This is the mathlib4 version of that pull request.

We define arbitrarily indexed products in a commutative monoid with a topology. This is done by "multiplicativizing" the currently existing definitions and theorems about arbitrarily indexed sums. That is, the existing code is rewritten in the multiplicative setting, and the original definitions and theorems are recovered using `@[to_additive]`. Please see this thread on Zulip for information on why this approach was chosen: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infinite.20products

As YaelDillies wrote in the description of leanprover-community/mathlib#18405, there are a few small technical issues that arise when directly "multiplicativizing" theorems in this way:
- I have renamed `cauchySeq_finset_iff_vanishing` to `cauchySeq_finset_iff_sum_vanishing` to make the name multiplicativizable. This is slightly different from the name `cauchy_seq_finset_sum_iff_vanishing` that YaelDillies used, and it is meant to parallel the existing name `cauchySeq_finset_iff_tsum_vanishing`.
- Currently, on master, there is a theorem called `tsum_sum` about taking the `tsum` of a `sum`, and a theorem called `tsum_prod` about taking a `tsum` on a product of two index sets. I have called the multiplicative versions `tprod_of_prod` and `tprod_prod`. This is slightly different from the names `tprod_prod''` and `tprod_prod` that YaelDillies used. eric-wieser suggested renaming `tsum_prod` to `tsum_prod_index` to get around this issue, which I can do in a separate pull request.

Mathlib/Analysis/Normed/Group/InfiniteSum.lean

@@ -40,7 +40,7 @@ variable {ι α E F : Type*} [SeminormedAddCommGroup E] [SeminormedAddCommGroup
 theorem cauchySeq_finset_iff_vanishing_norm {f : ι → E} :
     (CauchySeq fun s : Finset ι => ∑ i in s, f i) ↔
       ∀ ε > (0 : ℝ), ∃ s : Finset ι, ∀ t, Disjoint t s → ‖∑ i in t, f i‖ < ε := by
-  rw [cauchySeq_finset_iff_vanishing, nhds_basis_ball.forall_iff]
+  rw [cauchySeq_finset_iff_sum_vanishing, nhds_basis_ball.forall_iff]
   · simp only [ball_zero_eq, Set.mem_setOf_eq]
   · rintro s t hst ⟨s', hs'⟩
     exact ⟨s', fun t' ht' => hst <| hs' _ ht'⟩

Mathlib/Tactic/ToAdditive.lean

@@ -925,6 +925,7 @@ def nameDict : String → List String
   | "hdiv"        => ["hsub"]
   | "hpow"        => ["hsmul"]
   | "finprod"     => ["finsum"]
+  | "tprod"       => ["tsum"]
   | "pow"         => ["nsmul"]
   | "npow"        => ["nsmul"]
   | "zpow"        => ["zsmul"]
@@ -945,6 +946,7 @@ def nameDict : String → List String
   | "semiconj"    => ["add", "Semiconj"]
   | "zpowers"     => ["zmultiples"]
   | "powers"      => ["multiples"]
+  | "multipliable"=> ["summable"]
   | x             => [x]
 
 /--

Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean

@@ -9,8 +9,8 @@ import Mathlib.Topology.Algebra.Star
 /-!
 # Topological sums and functorial constructions
 
-Lemmas on the interaction of `tsum`, `HasSum` etc with products, Sigma and Pi types,
-`MulOpposite`, etc.
+Lemmas on the interaction of `tprod`, `tsum`, `HasProd`, `HasSum` etc with products, Sigma and Pi
+types, `MulOpposite`, etc.
 
 -/
 
@@ -27,83 +27,93 @@ variable {α β γ δ : Type*}
 
 section ProdDomain
 
-variable [AddCommMonoid α] [TopologicalSpace α]
+variable [CommMonoid α] [TopologicalSpace α]
 
-theorem hasSum_pi_single [DecidableEq β] (b : β) (a : α) : HasSum (Pi.single b a) a := by
-  convert hasSum_ite_eq b a
-  simp [Pi.single_apply]
+@[to_additive]
+theorem hasProd_pi_single [DecidableEq β] (b : β) (a : α) : HasProd (Pi.mulSingle b a) a := by
+  convert hasProd_ite_eq b a
+  simp [Pi.mulSingle_apply]
 #align has_sum_pi_single hasSum_pi_single
 
-@[simp]
-theorem tsum_pi_single [DecidableEq β] (b : β) (a : α) : ∑' b', Pi.single b a b' = a := by
-  rw [tsum_eq_single b]
+@[to_additive (attr := simp)]
+theorem tprod_pi_single [DecidableEq β] (b : β) (a : α) : ∏' b', Pi.mulSingle b a b' = a := by
+  rw [tprod_eq_mulSingle b]
   · simp
   · intro b' hb'; simp [hb']
 #align tsum_pi_single tsum_pi_single
 
-lemma tsum_setProd_singleton_left (b : β) (t : Set γ) (f : β × γ → α) :
-    (∑' x : {b} ×ˢ t, f x) = ∑' c : t, f (b, c) := by
-  rw [tsum_congr_set_coe _ Set.singleton_prod, tsum_image _ ((Prod.mk.inj_left b).injOn _)]
+@[to_additive tsum_setProd_singleton_left]
+lemma tprod_setProd_singleton_left (b : β) (t : Set γ) (f : β × γ → α) :
+    (∏' x : {b} ×ˢ t, f x) = ∏' c : t, f (b, c) := by
+  rw [tprod_congr_set_coe _ Set.singleton_prod, tprod_image _ ((Prod.mk.inj_left b).injOn _)]
 
-lemma tsum_setProd_singleton_right (s : Set β) (c : γ) (f : β × γ → α) :
-    (∑' x : s ×ˢ {c}, f x) = ∑' b : s, f (b, c) := by
-  rw [tsum_congr_set_coe _ Set.prod_singleton, tsum_image _ ((Prod.mk.inj_right c).injOn _)]
+@[to_additive tsum_setProd_singleton_right]
+lemma tprod_setProd_singleton_right (s : Set β) (c : γ) (f : β × γ → α) :
+    (∏' x : s ×ˢ {c}, f x) = ∏' b : s, f (b, c) := by
+  rw [tprod_congr_set_coe _ Set.prod_singleton, tprod_image _ ((Prod.mk.inj_right c).injOn _)]
 
-theorem Summable.prod_symm {f : β × γ → α} (hf : Summable f) : Summable fun p : γ × β ↦ f p.swap :=
-  (Equiv.prodComm γ β).summable_iff.2 hf
+@[to_additive Summable.prod_symm]
+theorem Multipliable.prod_symm {f : β × γ → α} (hf : Multipliable f) :
+    Multipliable fun p : γ × β ↦ f p.swap :=
+  (Equiv.prodComm γ β).multipliable_iff.2 hf
 #align summable.prod_symm Summable.prod_symm
 
 end ProdDomain
 
 section ProdCodomain
 
-variable [AddCommMonoid α] [TopologicalSpace α] [AddCommMonoid γ] [TopologicalSpace γ]
+variable [CommMonoid α] [TopologicalSpace α] [CommMonoid γ] [TopologicalSpace γ]
 
-theorem HasSum.prod_mk {f : β → α} {g : β → γ} {a : α} {b : γ} (hf : HasSum f a) (hg : HasSum g b) :
-    HasSum (fun x ↦ (⟨f x, g x⟩ : α × γ)) ⟨a, b⟩ := by
-  simp [HasSum, ← prod_mk_sum, Filter.Tendsto.prod_mk_nhds hf hg]
+@[to_additive HasSum.prod_mk]
+theorem HasProd.prod_mk {f : β → α} {g : β → γ} {a : α} {b : γ}
+    (hf : HasProd f a) (hg : HasProd g b) : HasProd (fun x ↦ (⟨f x, g x⟩ : α × γ)) ⟨a, b⟩ := by
+  simp [HasProd, ← prod_mk_prod, Filter.Tendsto.prod_mk_nhds hf hg]
 #align has_sum.prod_mk HasSum.prod_mk
 
 end ProdCodomain
 
-section ContinuousAdd
+section ContinuousMul
 
-variable [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α]
+variable [CommMonoid α] [TopologicalSpace α] [ContinuousMul α]
 
 section RegularSpace
 
 variable [RegularSpace α]
 
-theorem HasSum.sigma {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α}
-    (ha : HasSum f a) (hf : ∀ b, HasSum (fun c ↦ f ⟨b, c⟩) (g b)) : HasSum g a := by
+@[to_additive]
+theorem HasProd.sigma {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α}
+    (ha : HasProd f a) (hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) : HasProd g a := by
   classical
   refine' (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr _
   rintro s ⟨hs, hsc⟩
   rcases mem_atTop_sets.mp (ha hs) with ⟨u, hu⟩
   use u.image Sigma.fst, trivial
   intro bs hbs
   simp only [Set.mem_preimage, ge_iff_le, Finset.le_iff_subset] at hu
-  have : Tendsto (fun t : Finset (Σb, γ b) ↦ ∑ p in t.filter fun p ↦ p.1 ∈ bs, f p) atTop
-      (𝓝 <| ∑ b in bs, g b) := by
-    simp only [← sigma_preimage_mk, sum_sigma]
-    refine' tendsto_finset_sum _ fun b _ ↦ _
+  have : Tendsto (fun t : Finset (Σb, γ b) ↦ ∏ p in t.filter fun p ↦ p.1 ∈ bs, f p) atTop
+      (𝓝 <| ∏ b in bs, g b) := by
+    simp only [← sigma_preimage_mk, prod_sigma]
+    refine' tendsto_finset_prod _ fun b _ ↦ _
     change
-      Tendsto (fun t ↦ (fun t ↦ ∑ s in t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
+      Tendsto (fun t ↦ (fun t ↦ ∏ s in t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
     exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
   refine' hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ _⟩)
   exact mem_filter.2 ⟨ht hx, hbs <| mem_image_of_mem _ hx⟩
 #align has_sum.sigma HasSum.sigma
 
-/-- If a series `f` on `β × γ` has sum `a` and for each `b` the restriction of `f` to `{b} × γ`
-has sum `g b`, then the series `g` has sum `a`. -/
-theorem HasSum.prod_fiberwise {f : β × γ → α} {g : β → α} {a : α} (ha : HasSum f a)
-    (hf : ∀ b, HasSum (fun c ↦ f (b, c)) (g b)) : HasSum g a :=
-  HasSum.sigma ((Equiv.sigmaEquivProd β γ).hasSum_iff.2 ha) hf
+/-- If a function `f` on `β × γ` has product `a` and for each `b` the restriction of `f` to
+`{b} × γ` has product `g b`, then the function `g` has product `a`. -/
+@[to_additive HasSum.prod_fiberwise "If a series `f` on `β × γ` has sum `a` and for each `b` the
+restriction of `f` to `{b} × γ` has sum `g b`, then the series `g` has sum `a`."]
+theorem HasProd.prod_fiberwise {f : β × γ → α} {g : β → α} {a : α} (ha : HasProd f a)
+    (hf : ∀ b, HasProd (fun c ↦ f (b, c)) (g b)) : HasProd g a :=
+  HasProd.sigma ((Equiv.sigmaEquivProd β γ).hasProd_iff.2 ha) hf
 #align has_sum.prod_fiberwise HasSum.prod_fiberwise
 
-theorem Summable.sigma' {γ : β → Type*} {f : (Σb : β, γ b) → α} (ha : Summable f)
-    (hf : ∀ b, Summable fun c ↦ f ⟨b, c⟩) : Summable fun b ↦ ∑' c, f ⟨b, c⟩ :=
-  (ha.hasSum.sigma fun b ↦ (hf b).hasSum).summable
+@[to_additive]
+theorem Multipliable.sigma' {γ : β → Type*} {f : (Σb : β, γ b) → α} (ha : Multipliable f)
+    (hf : ∀ b, Multipliable fun c ↦ f ⟨b, c⟩) : Multipliable fun b ↦ ∏' c, f ⟨b, c⟩ :=
+  (ha.hasProd.sigma fun b ↦ (hf b).hasProd).multipliable
 #align summable.sigma' Summable.sigma'
 
 end RegularSpace
@@ -112,72 +122,88 @@ section T3Space
 
 variable [T3Space α]
 
-theorem HasSum.sigma_of_hasSum {γ : β → Type*} {f : (Σb : β, γ b) → α} {g : β → α}
-    {a : α} (ha : HasSum g a) (hf : ∀ b, HasSum (fun c ↦ f ⟨b, c⟩) (g b)) (hf' : Summable f) :
-    HasSum f a := by simpa [(hf'.hasSum.sigma hf).unique ha] using hf'.hasSum
+@[to_additive]
+theorem HasProd.sigma_of_hasProd {γ : β → Type*} {f : (Σb : β, γ b) → α} {g : β → α}
+    {a : α} (ha : HasProd g a) (hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) (hf' : Multipliable f) :
+    HasProd f a := by simpa [(hf'.hasProd.sigma hf).unique ha] using hf'.hasProd
 #align has_sum.sigma_of_has_sum HasSum.sigma_of_hasSum
 
-theorem tsum_sigma' {γ : β → Type*} {f : (Σb : β, γ b) → α} (h₁ : ∀ b, Summable fun c ↦ f ⟨b, c⟩)
-    (h₂ : Summable f) : ∑' p, f p = ∑' (b) (c), f ⟨b, c⟩ :=
-  (h₂.hasSum.sigma fun b ↦ (h₁ b).hasSum).tsum_eq.symm
+@[to_additive]
+theorem tprod_sigma' {γ : β → Type*} {f : (Σb : β, γ b) → α}
+    (h₁ : ∀ b, Multipliable fun c ↦ f ⟨b, c⟩) (h₂ : Multipliable f) :
+    ∏' p, f p = ∏' (b) (c), f ⟨b, c⟩ :=
+  (h₂.hasProd.sigma fun b ↦ (h₁ b).hasProd).tprod_eq.symm
 #align tsum_sigma' tsum_sigma'
 
-theorem tsum_prod' {f : β × γ → α} (h : Summable f) (h₁ : ∀ b, Summable fun c ↦ f (b, c)) :
-    ∑' p, f p = ∑' (b) (c), f (b, c) :=
-  (h.hasSum.prod_fiberwise fun b ↦ (h₁ b).hasSum).tsum_eq.symm
+@[to_additive tsum_prod']
+theorem tprod_prod' {f : β × γ → α} (h : Multipliable f)
+    (h₁ : ∀ b, Multipliable fun c ↦ f (b, c)) :
+    ∏' p, f p = ∏' (b) (c), f (b, c) :=
+  (h.hasProd.prod_fiberwise fun b ↦ (h₁ b).hasProd).tprod_eq.symm
 #align tsum_prod' tsum_prod'
 
-theorem tsum_comm' {f : β → γ → α} (h : Summable (Function.uncurry f)) (h₁ : ∀ b, Summable (f b))
-    (h₂ : ∀ c, Summable fun b ↦ f b c) : ∑' (c) (b), f b c = ∑' (b) (c), f b c := by
-  erw [← tsum_prod' h h₁, ← tsum_prod' h.prod_symm h₂, ← (Equiv.prodComm γ β).tsum_eq (uncurry f)]
+@[to_additive]
+theorem tprod_comm' {f : β → γ → α} (h : Multipliable (Function.uncurry f))
+    (h₁ : ∀ b, Multipliable (f b)) (h₂ : ∀ c, Multipliable fun b ↦ f b c) :
+    ∏' (c) (b), f b c = ∏' (b) (c), f b c := by
+  erw [← tprod_prod' h h₁, ← tprod_prod' h.prod_symm h₂,
+      ← (Equiv.prodComm γ β).tprod_eq (uncurry f)]
   rfl
 #align tsum_comm' tsum_comm'
 
 end T3Space
 
-end ContinuousAdd
+end ContinuousMul
 
 section CompleteSpace
 
-variable [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α]
+variable [CommGroup α] [UniformSpace α] [UniformGroup α] [CompleteSpace α]
 
-theorem Summable.sigma_factor {γ : β → Type*} {f : (Σb : β, γ b) → α} (ha : Summable f) (b : β) :
-    Summable fun c ↦ f ⟨b, c⟩ :=
+@[to_additive]
+theorem Multipliable.sigma_factor {γ : β → Type*} {f : (Σb : β, γ b) → α}
+    (ha : Multipliable f) (b : β) :
+    Multipliable fun c ↦ f ⟨b, c⟩ :=
   ha.comp_injective sigma_mk_injective
 #align summable.sigma_factor Summable.sigma_factor
 
-theorem Summable.sigma {γ : β → Type*} {f : (Σb : β, γ b) → α} (ha : Summable f) :
-    Summable fun b ↦ ∑' c, f ⟨b, c⟩ :=
+@[to_additive]
+theorem Multipliable.sigma {γ : β → Type*} {f : (Σb : β, γ b) → α} (ha : Multipliable f) :
+    Multipliable fun b ↦ ∏' c, f ⟨b, c⟩ :=
   ha.sigma' fun b ↦ ha.sigma_factor b
 #align summable.sigma Summable.sigma
 
-theorem Summable.prod_factor {f : β × γ → α} (h : Summable f) (b : β) :
-    Summable fun c ↦ f (b, c) :=
+@[to_additive Summable.prod_factor]
+theorem Multipliable.prod_factor {f : β × γ → α} (h : Multipliable f) (b : β) :
+    Multipliable fun c ↦ f (b, c) :=
   h.comp_injective fun _ _ h ↦ (Prod.ext_iff.1 h).2
 #align summable.prod_factor Summable.prod_factor
 
-lemma HasSum.tsum_fiberwise [T2Space α] {f : β → α} {a : α} (hf : HasSum f a) (g : β → γ) :
-    HasSum (fun c : γ ↦ ∑' b : g ⁻¹' {c}, f b) a :=
-  (((Equiv.sigmaFiberEquiv g).hasSum_iff).mpr hf).sigma <|
-    fun _ ↦ ((hf.summable.subtype _).hasSum_iff).mpr rfl
+@[to_additive]
+lemma HasProd.tprod_fiberwise [T2Space α] {f : β → α} {a : α} (hf : HasProd f a) (g : β → γ) :
+    HasProd (fun c : γ ↦ ∏' b : g ⁻¹' {c}, f b) a :=
+  (((Equiv.sigmaFiberEquiv g).hasProd_iff).mpr hf).sigma <|
+    fun _ ↦ ((hf.multipliable.subtype _).hasProd_iff).mpr rfl
 
 section CompleteT0Space
 
 variable [T0Space α]
 
-theorem tsum_sigma {γ : β → Type*} {f : (Σb : β, γ b) → α} (ha : Summable f) :
-    ∑' p, f p = ∑' (b) (c), f ⟨b, c⟩ :=
-  tsum_sigma' (fun b ↦ ha.sigma_factor b) ha
+@[to_additive]
+theorem tprod_sigma {γ : β → Type*} {f : (Σb : β, γ b) → α} (ha : Multipliable f) :
+    ∏' p, f p = ∏' (b) (c), f ⟨b, c⟩ :=
+  tprod_sigma' (fun b ↦ ha.sigma_factor b) ha
 #align tsum_sigma tsum_sigma
 
-theorem tsum_prod {f : β × γ → α} (h : Summable f) :
-    ∑' p, f p = ∑' (b) (c), f ⟨b, c⟩ :=
-  tsum_prod' h h.prod_factor
+@[to_additive tsum_prod]
+theorem tprod_prod {f : β × γ → α} (h : Multipliable f) :
+    ∏' p, f p = ∏' (b) (c), f ⟨b, c⟩ :=
+  tprod_prod' h h.prod_factor
 #align tsum_prod tsum_prod
 
-theorem tsum_comm {f : β → γ → α} (h : Summable (Function.uncurry f)) :
-    ∑' (c) (b), f b c = ∑' (b) (c), f b c :=
-  tsum_comm' h h.prod_factor h.prod_symm.prod_factor
+@[to_additive]
+theorem tprod_comm {f : β → γ → α} (h : Multipliable (Function.uncurry f)) :
+    ∏' (c) (b), f b c = ∏' (b) (c), f b c :=
+  tprod_comm' h h.prod_factor h.prod_symm.prod_factor
 #align tsum_comm tsum_comm
 
 end CompleteT0Space
@@ -186,20 +212,23 @@ end CompleteSpace
 
 section Pi
 
-variable {ι : Type*} {π : α → Type*} [∀ x, AddCommMonoid (π x)] [∀ x, TopologicalSpace (π x)]
+variable {ι : Type*} {π : α → Type*} [∀ x, CommMonoid (π x)] [∀ x, TopologicalSpace (π x)]
 
-theorem Pi.hasSum {f : ι → ∀ x, π x} {g : ∀ x, π x} :
-    HasSum f g ↔ ∀ x, HasSum (fun i ↦ f i x) (g x) := by
-  simp only [HasSum, tendsto_pi_nhds, sum_apply]
+@[to_additive]
+theorem Pi.hasProd {f : ι → ∀ x, π x} {g : ∀ x, π x} :
+    HasProd f g ↔ ∀ x, HasProd (fun i ↦ f i x) (g x) := by
+  simp only [HasProd, tendsto_pi_nhds, prod_apply]
 #align pi.has_sum Pi.hasSum
 
-theorem Pi.summable {f : ι → ∀ x, π x} : Summable f ↔ ∀ x, Summable fun i ↦ f i x := by
-  simp only [Summable, Pi.hasSum, Classical.skolem]
+@[to_additive]
+theorem Pi.multipliable {f : ι → ∀ x, π x} : Multipliable f ↔ ∀ x, Multipliable fun i ↦ f i x := by
+  simp only [Multipliable, Pi.hasProd, Classical.skolem]
 #align pi.summable Pi.summable
 
-theorem tsum_apply [∀ x, T2Space (π x)] {f : ι → ∀ x, π x} {x : α} (hf : Summable f) :
-    (∑' i, f i) x = ∑' i, f i x :=
-  (Pi.hasSum.mp hf.hasSum x).tsum_eq.symm
+@[to_additive]
+theorem tprod_apply [∀ x, T2Space (π x)] {f : ι → ∀ x, π x} {x : α} (hf : Multipliable f) :
+    (∏' i, f i) x = ∏' i, f i x :=
+  (Pi.hasProd.mp hf.hasProd x).tprod_eq.symm
 #align tsum_apply tsum_apply
 
 end Pi