Infinite sums and products in topological groups

Lemmas on topological sums in groups (as opposed to monoids).

theorem HasProd.inv {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} {a : α} (h : HasProd f a) : HasProd (fun (b : β) => (f b)⁻¹) a⁻¹

theorem HasSum.neg {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} {a : α} (h : HasSum f a) : HasSum (fun (b : β) => -f b) (-a)

theorem Multipliable.inv {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} (hf : Multipliable f) : Multipliable fun (b : β) => (f b)⁻¹

theorem Summable.neg {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} (hf : Summable f) : Summable fun (b : β) => -f b

theorem Multipliable.of_inv {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} (hf : Multipliable fun (b : β) => (f b)⁻¹) : Multipliable f

theorem Summable.of_neg {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} (hf : Summable fun (b : β) => -f b) : Summable f

theorem multipliable_inv_iff {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} : (Multipliable fun (b : β) => (f b)⁻¹) ↔ Multipliable f

theorem summable_neg_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} : (Summable fun (b : β) => -f b) ↔ Summable f

theorem HasProd.div {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f g : β → α} {a₁ a₂ : α} (hf : HasProd f a₁) (hg : HasProd g a₂) : HasProd (fun (b : β) => f b / g b) (a₁ / a₂)

theorem HasSum.sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f g : β → α} {a₁ a₂ : α} (hf : HasSum f a₁) (hg : HasSum g a₂) : HasSum (fun (b : β) => f b - g b) (a₁ - a₂)

theorem Multipliable.div {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f g : β → α} (hf : Multipliable f) (hg : Multipliable g) : Multipliable fun (b : β) => f b / g b

theorem Summable.sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f g : β → α} (hf : Summable f) (hg : Summable g) : Summable fun (b : β) => f b - g b

theorem Multipliable.trans_div {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f g : β → α} (hg : Multipliable g) (hfg : Multipliable fun (b : β) => f b / g b) : Multipliable f

theorem Summable.trans_sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f g : β → α} (hg : Summable g) (hfg : Summable fun (b : β) => f b - g b) : Summable f

theorem multipliable_iff_of_multipliable_div {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f g : β → α} (hfg : Multipliable fun (b : β) => f b / g b) : Multipliable f ↔ Multipliable g

theorem summable_iff_of_summable_sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f g : β → α} (hfg : Summable fun (b : β) => f b - g b) : Summable f ↔ Summable g

theorem HasProd.update {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} {a₁ : α} (hf : HasProd f a₁) (b : β) [DecidableEq β] (a : α) : HasProd (Function.update f b a) (a / f b * a₁)

theorem HasSum.update {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} {a₁ : α} (hf : HasSum f a₁) (b : β) [DecidableEq β] (a : α) : HasSum (Function.update f b a) (a - f b + a₁)

theorem Multipliable.update {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} (hf : Multipliable f) (b : β) [DecidableEq β] (a : α) : Multipliable (Function.update f b a)

theorem Summable.update {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} (hf : Summable f) (b : β) [DecidableEq β] (a : α) : Summable (Function.update f b a)

theorem HasProd.hasProd_compl_iff {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} {a₁ a₂ : α} {s : Set β} (hf : HasProd (f ∘ Subtype.val) a₁) : HasProd (f ∘ Subtype.val) a₂ ↔ HasProd f (a₁ * a₂)

theorem HasSum.hasSum_compl_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} {a₁ a₂ : α} {s : Set β} (hf : HasSum (f ∘ Subtype.val) a₁) : HasSum (f ∘ Subtype.val) a₂ ↔ HasSum f (a₁ + a₂)

theorem HasProd.hasProd_iff_compl {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} {a₁ a₂ : α} {s : Set β} (hf : HasProd (f ∘ Subtype.val) a₁) : HasProd f a₂ ↔ HasProd (f ∘ Subtype.val) (a₂ / a₁)

theorem HasSum.hasSum_iff_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} {a₁ a₂ : α} {s : Set β} (hf : HasSum (f ∘ Subtype.val) a₁) : HasSum f a₂ ↔ HasSum (f ∘ Subtype.val) (a₂ - a₁)

theorem Multipliable.multipliable_compl_iff {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} {s : Set β} (hf : Multipliable (f ∘ Subtype.val)) : Multipliable (f ∘ Subtype.val) ↔ Multipliable f

theorem Summable.summable_compl_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} {s : Set β} (hf : Summable (f ∘ Subtype.val)) : Summable (f ∘ Subtype.val) ↔ Summable f

theorem Finset.hasProd_compl_iff {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} {a : α} (s : Finset β) : HasProd (fun (x : { x : β // x ∉ s }) => f ↑x) a ↔ HasProd f (a * ∏ i ∈ s, f i)

theorem Finset.hasSum_compl_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} {a : α} (s : Finset β) : HasSum (fun (x : { x : β // x ∉ s }) => f ↑x) a ↔ HasSum f (a + ∑ i ∈ s, f i)

theorem Finset.hasProd_iff_compl {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} {a : α} (s : Finset β) : HasProd f a ↔ HasProd (fun (x : { x : β // x ∉ s }) => f ↑x) (a / ∏ i ∈ s, f i)

theorem Finset.hasSum_iff_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} {a : α} (s : Finset β) : HasSum f a ↔ HasSum (fun (x : { x : β // x ∉ s }) => f ↑x) (a - ∑ i ∈ s, f i)

theorem Finset.multipliable_compl_iff {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} (s : Finset β) : (Multipliable fun (x : { x : β // x ∉ s }) => f ↑x) ↔ Multipliable f

theorem Finset.summable_compl_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} (s : Finset β) : (Summable fun (x : { x : β // x ∉ s }) => f ↑x) ↔ Summable f

theorem Set.Finite.multipliable_compl_iff {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} {s : Set β} (hs : s.Finite) : Multipliable (f ∘ Subtype.val) ↔ Multipliable f

theorem Set.Finite.summable_compl_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} {s : Set β} (hs : s.Finite) : Summable (f ∘ Subtype.val) ↔ Summable f

theorem hasProd_ite_div_hasProd {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} {a : α} [DecidableEq β] (hf : HasProd f a) (b : β) : HasProd (fun (n : β) => if n = b then 1 else f n) (a / f b)

theorem hasSum_ite_sub_hasSum {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} {a : α} [DecidableEq β] (hf : HasSum f a) (b : β) : HasSum (fun (n : β) => if n = b then 0 else f n) (a - f b)

theorem Multipliable.congr_cofinite {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f g : β → α} (hf : Multipliable f) (hfg : f =ᶠ[Filter.cofinite] g) : Multipliable g

A more general version of Multipliable.congr, allowing the functions to disagree on a finite set.

Note that this requires the target to be a group, and hence fails for products valued in a ring. See Multipliable.congr_cofinite₀ for a version applying in this case, with an additional non-vanishing hypothesis.

theorem Summable.congr_cofinite {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f g : β → α} (hf : Summable f) (hfg : f =ᶠ[Filter.cofinite] g) : Summable g

A more general version of Summable.congr, allowing the functions to disagree on a finite set.

theorem multipliable_congr_cofinite {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f g : β → α} (hfg : f =ᶠ[Filter.cofinite] g) : Multipliable f ↔ Multipliable g

A more general version of multipliable_congr, allowing the functions to disagree on a finite set.

theorem summable_congr_cofinite {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f g : β → α} (hfg : f =ᶠ[Filter.cofinite] g) : Summable f ↔ Summable g

A more general version of summable_congr, allowing the functions to disagree on a finite set.

theorem Multipliable.congr_atTop {α : Type u_1} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f₁ g₁ : ℕ → α} (hf : Multipliable f₁) (hfg : f₁ =ᶠ[Filter.atTop] g₁) : Multipliable g₁

theorem Summable.congr_atTop {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f₁ g₁ : ℕ → α} (hf : Summable f₁) (hfg : f₁ =ᶠ[Filter.atTop] g₁) : Summable g₁

theorem multipliable_congr_atTop {α : Type u_1} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f₁ g₁ : ℕ → α} (hfg : f₁ =ᶠ[Filter.atTop] g₁) : Multipliable f₁ ↔ Multipliable g₁

theorem summable_congr_atTop {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f₁ g₁ : ℕ → α} (hfg : f₁ =ᶠ[Filter.atTop] g₁) : Summable f₁ ↔ Summable g₁

theorem tprod_inv {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} [T2Space α] : ∏' (b : β), (f b)⁻¹ = (∏' (b : β), f b)⁻¹

theorem tsum_neg {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} [T2Space α] : ∑' (b : β), -f b = -∑' (b : β), f b

theorem Multipliable.tprod_div {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f g : β → α} [T2Space α] (hf : Multipliable f) (hg : Multipliable g) : ∏' (b : β), f b / g b = (∏' (b : β), f b) / ∏' (b : β), g b

theorem Summable.tsum_sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f g : β → α} [T2Space α] (hf : Summable f) (hg : Summable g) : ∑' (b : β), (f b - g b) = ∑' (b : β), f b - ∑' (b : β), g b

@[deprecated Summable.tsum_sub (since := "2025-04-12")]

theorem tsum_sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f g : β → α} [T2Space α] (hf : Summable f) (hg : Summable g) : ∑' (b : β), (f b - g b) = ∑' (b : β), f b - ∑' (b : β), g b

Alias of Summable.tsum_sub.

@[deprecated Multipliable.tprod_div (since := "2025-04-12")]

theorem tprod_div {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f g : β → α} [T2Space α] (hf : Multipliable f) (hg : Multipliable g) : ∏' (b : β), f b / g b = (∏' (b : β), f b) / ∏' (b : β), g b

Alias of Multipliable.tprod_div.

theorem Multipliable.prod_mul_tprod_compl {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} [T2Space α] {s : Finset β} (hf : Multipliable f) : (∏ x ∈ s, f x) * ∏' (x : ↑(↑s)ᶜ), f ↑x = ∏' (x : β), f x

theorem Summable.sum_add_tsum_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} [T2Space α] {s : Finset β} (hf : Summable f) : ∑ x ∈ s, f x + ∑' (x : ↑(↑s)ᶜ), f ↑x = ∑' (x : β), f x

@[deprecated Summable.sum_add_tsum_compl (since := "2025-04-12")]

theorem sum_add_tsum_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} [T2Space α] {s : Finset β} (hf : Summable f) : ∑ x ∈ s, f x + ∑' (x : ↑(↑s)ᶜ), f ↑x = ∑' (x : β), f x

Alias of Summable.sum_add_tsum_compl.

@[deprecated Multipliable.prod_mul_tprod_compl (since := "2025-04-12")]

theorem prod_mul_tprod_compl {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} [T2Space α] {s : Finset β} (hf : Multipliable f) : (∏ x ∈ s, f x) * ∏' (x : ↑(↑s)ᶜ), f ↑x = ∏' (x : β), f x

Alias of Multipliable.prod_mul_tprod_compl.

theorem Multipliable.tprod_eq_mul_tprod_ite {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} [T2Space α] [DecidableEq β] (hf : Multipliable f) (b : β) : ∏' (n : β), f n = f b * ∏' (n : β), if n = b then 1 else f n

Let f : β → α be a multipliable function and let b ∈ β be an index. Lemma tprod_eq_mul_tprod_ite writes ∏ n, f n as f b times the product of the remaining terms.

theorem Summable.tsum_eq_add_tsum_ite {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} [T2Space α] [DecidableEq β] (hf : Summable f) (b : β) : ∑' (n : β), f n = f b + ∑' (n : β), if n = b then 0 else f n

Let f : β → α be a summable function and let b ∈ β be an index. Lemma tsum_eq_add_tsum_ite writes Σ' n, f n as f b plus the sum of the remaining terms.

@[deprecated Summable.tsum_eq_add_tsum_ite (since := "2025-04-12")]

theorem tsum_eq_add_tsum_ite {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} [T2Space α] [DecidableEq β] (hf : Summable f) (b : β) : ∑' (n : β), f n = f b + ∑' (n : β), if n = b then 0 else f n

Alias of Summable.tsum_eq_add_tsum_ite.

---

Let f : β → α be a summable function and let b ∈ β be an index. Lemma tsum_eq_add_tsum_ite writes Σ' n, f n as f b plus the sum of the remaining terms.

@[deprecated Multipliable.tprod_eq_mul_tprod_ite (since := "2025-04-12")]

theorem tprod_eq_mul_tprod_ite {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} [T2Space α] [DecidableEq β] (hf : Multipliable f) (b : β) : ∏' (n : β), f n = f b * ∏' (n : β), if n = b then 1 else f n

Alias of Multipliable.tprod_eq_mul_tprod_ite.

---

Let f : β → α be a multipliable function and let b ∈ β be an index. Lemma tprod_eq_mul_tprod_ite writes ∏ n, f n as f b times the product of the remaining terms.

theorem multipliable_iff_cauchySeq_finset {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [CompleteSpace α] {f : β → α} : Multipliable f ↔ CauchySeq fun (s : Finset β) => ∏ b ∈ s, f b

The Cauchy criterion for infinite products, also known as the Cauchy convergence test

theorem summable_iff_cauchySeq_finset {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [CompleteSpace α] {f : β → α} : Summable f ↔ CauchySeq fun (s : Finset β) => ∑ b ∈ s, f b

The Cauchy criterion for infinite sums, also known as the Cauchy convergence test

theorem cauchySeq_finset_iff_prod_vanishing {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] {f : β → α} : (CauchySeq fun (s : Finset β) => ∏ b ∈ s, f b) ↔ ∀ e ∈ nhds 1, ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

theorem cauchySeq_finset_iff_sum_vanishing {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] {f : β → α} : (CauchySeq fun (s : Finset β) => ∑ b ∈ s, f b) ↔ ∀ e ∈ nhds 0, ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∑ b ∈ t, f b ∈ e

theorem cauchySeq_finset_iff_tprod_vanishing {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] {f : β → α} : (CauchySeq fun (s : Finset β) => ∏ b ∈ s, f b) ↔ ∀ e ∈ nhds 1, ∃ (s : Finset β), ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

theorem cauchySeq_finset_iff_tsum_vanishing {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] {f : β → α} : (CauchySeq fun (s : Finset β) => ∑ b ∈ s, f b) ↔ ∀ e ∈ nhds 0, ∃ (s : Finset β), ∀ (t : Set β), Disjoint t ↑s → ∑' (b : ↑t), f ↑b ∈ e

theorem multipliable_iff_vanishing {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] {f : β → α} [CompleteSpace α] : Multipliable f ↔ ∀ e ∈ nhds 1, ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

theorem summable_iff_vanishing {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] {f : β → α} [CompleteSpace α] : Summable f ↔ ∀ e ∈ nhds 0, ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t s → ∑ b ∈ t, f b ∈ e

theorem multipliable_iff_tprod_vanishing {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] {f : β → α} [CompleteSpace α] : Multipliable f ↔ ∀ e ∈ nhds 1, ∃ (s : Finset β), ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

theorem summable_iff_tsum_vanishing {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] {f : β → α} [CompleteSpace α] : Summable f ↔ ∀ e ∈ nhds 0, ∃ (s : Finset β), ∀ (t : Set β), Disjoint t ↑s → ∑' (b : ↑t), f ↑b ∈ e

theorem Multipliable.multipliable_of_eq_one_or_self {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] {f g : β → α} [CompleteSpace α] (hf : Multipliable f) (h : ∀ (b : β), g b = 1 ∨ g b = f b) : Multipliable g

theorem Summable.summable_of_eq_zero_or_self {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] {f g : β → α} [CompleteSpace α] (hf : Summable f) (h : ∀ (b : β), g b = 0 ∨ g b = f b) : Summable g

theorem Multipliable.mulIndicator {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] {f : β → α} [CompleteSpace α] (hf : Multipliable f) (s : Set β) : Multipliable (s.mulIndicator f)

theorem Summable.indicator {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] {f : β → α} [CompleteSpace α] (hf : Summable f) (s : Set β) : Summable (s.indicator f)

theorem Multipliable.comp_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommGroup α] [UniformSpace α] [IsUniformGroup α] {f : β → α} [CompleteSpace α] {i : γ → β} (hf : Multipliable f) (hi : Function.Injective i) : Multipliable (f ∘ i)

theorem Summable.comp_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] {f : β → α} [CompleteSpace α] {i : γ → β} (hf : Summable f) (hi : Function.Injective i) : Summable (f ∘ i)

theorem Multipliable.subtype {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] {f : β → α} [CompleteSpace α] (hf : Multipliable f) (s : Set β) : Multipliable (f ∘ Subtype.val)

theorem Summable.subtype {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] {f : β → α} [CompleteSpace α] (hf : Summable f) (s : Set β) : Summable (f ∘ Subtype.val)

theorem multipliable_subtype_and_compl {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] {f : β → α} [CompleteSpace α] {s : Set β} : ((Multipliable fun (x : ↑s) => f ↑x) ∧ Multipliable fun (x : ↑sᶜ) => f ↑x) ↔ Multipliable f

theorem summable_subtype_and_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] {f : β → α} [CompleteSpace α] {s : Set β} : ((Summable fun (x : ↑s) => f ↑x) ∧ Summable fun (x : ↑sᶜ) => f ↑x) ↔ Summable f

theorem Multipliable.tprod_subtype_mul_tprod_subtype_compl {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] [T2Space α] {f : β → α} (hf : Multipliable f) (s : Set β) : (∏' (x : ↑s), f ↑x) * ∏' (x : ↑sᶜ), f ↑x = ∏' (x : β), f x

theorem Summable.tsum_subtype_add_tsum_subtype_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T2Space α] {f : β → α} (hf : Summable f) (s : Set β) : ∑' (x : ↑s), f ↑x + ∑' (x : ↑sᶜ), f ↑x = ∑' (x : β), f x

@[deprecated Summable.tsum_subtype_add_tsum_subtype_compl (since := "2025-04-12")]

theorem tsum_subtype_add_tsum_subtype_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T2Space α] {f : β → α} (hf : Summable f) (s : Set β) : ∑' (x : ↑s), f ↑x + ∑' (x : ↑sᶜ), f ↑x = ∑' (x : β), f x

Alias of Summable.tsum_subtype_add_tsum_subtype_compl.

@[deprecated Multipliable.tprod_subtype_mul_tprod_subtype_compl (since := "2025-04-12")]

theorem tprod_subtype_mul_tprod_subtype_compl {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] [T2Space α] {f : β → α} (hf : Multipliable f) (s : Set β) : (∏' (x : ↑s), f ↑x) * ∏' (x : ↑sᶜ), f ↑x = ∏' (x : β), f x

Alias of Multipliable.tprod_subtype_mul_tprod_subtype_compl.

theorem Multipliable.prod_mul_tprod_subtype_compl {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] [T2Space α] {f : β → α} (hf : Multipliable f) (s : Finset β) : (∏ x ∈ s, f x) * ∏' (x : { x : β // x ∉ s }), f ↑x = ∏' (x : β), f x

theorem Summable.sum_add_tsum_subtype_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T2Space α] {f : β → α} (hf : Summable f) (s : Finset β) : ∑ x ∈ s, f x + ∑' (x : { x : β // x ∉ s }), f ↑x = ∑' (x : β), f x

@[deprecated Summable.sum_add_tsum_subtype_compl (since := "2025-04-12")]

theorem sum_add_tsum_subtype_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T2Space α] {f : β → α} (hf : Summable f) (s : Finset β) : ∑ x ∈ s, f x + ∑' (x : { x : β // x ∉ s }), f ↑x = ∑' (x : β), f x

Alias of Summable.sum_add_tsum_subtype_compl.

@[deprecated Multipliable.prod_mul_tprod_subtype_compl (since := "2025-04-12")]

theorem prod_mul_tprod_subtype_compl {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] [CompleteSpace α] [T2Space α] {f : β → α} (hf : Multipliable f) (s : Finset β) : (∏ x ∈ s, f x) * ∏' (x : { x : β // x ∉ s }), f ↑x = ∏' (x : β), f x

Alias of Multipliable.prod_mul_tprod_subtype_compl.

theorem Multipliable.vanishing {α : Type u_1} {G : Type u_4} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] {f : α → G} (hf : Multipliable f) ⦃e : Set G⦄ (he : e ∈ nhds 1) : ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e

theorem Summable.vanishing {α : Type u_1} {G : Type u_4} [TopologicalSpace G] [AddCommGroup G] [IsTopologicalAddGroup G] {f : α → G} (hf : Summable f) ⦃e : Set G⦄ (he : e ∈ nhds 0) : ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t s → ∑ k ∈ t, f k ∈ e

theorem Multipliable.tprod_vanishing {α : Type u_1} {G : Type u_4} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] {f : α → G} (hf : Multipliable f) ⦃e : Set G⦄ (he : e ∈ nhds 1) : ∃ (s : Finset α), ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

theorem Summable.tsum_vanishing {α : Type u_1} {G : Type u_4} [TopologicalSpace G] [AddCommGroup G] [IsTopologicalAddGroup G] {f : α → G} (hf : Summable f) ⦃e : Set G⦄ (he : e ∈ nhds 0) : ∃ (s : Finset α), ∀ (t : Set α), Disjoint t ↑s → ∑' (b : ↑t), f ↑b ∈ e

theorem tendsto_tprod_compl_atTop_one {α : Type u_1} {G : Type u_4} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] (f : α → G) : Filter.Tendsto (fun (s : Finset α) => ∏' (a : { x : α // x ∉ s }), f ↑a) Filter.atTop (nhds 1)

The product over the complement of a finset tends to 1 when the finset grows to cover the whole space. This does not need a multipliability assumption, as otherwise all such products are one.

theorem tendsto_tsum_compl_atTop_zero {α : Type u_1} {G : Type u_4} [TopologicalSpace G] [AddCommGroup G] [IsTopologicalAddGroup G] (f : α → G) : Filter.Tendsto (fun (s : Finset α) => ∑' (a : { x : α // x ∉ s }), f ↑a) Filter.atTop (nhds 0)

The sum over the complement of a finset tends to 0 when the finset grows to cover the whole space. This does not need a summability assumption, as otherwise all such sums are zero.

theorem Multipliable.tendsto_cofinite_one {α : Type u_1} {G : Type u_4} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] {f : α → G} (hf : Multipliable f) : Filter.Tendsto f Filter.cofinite (nhds 1)

Product divergence test: if f is unconditionally multipliable, then f x tends to one along cofinite.

theorem Summable.tendsto_cofinite_zero {α : Type u_1} {G : Type u_4} [TopologicalSpace G] [AddCommGroup G] [IsTopologicalAddGroup G] {f : α → G} (hf : Summable f) : Filter.Tendsto f Filter.cofinite (nhds 0)

Series divergence test: if f is unconditionally summable, then f x tends to zero along cofinite.

theorem Multipliable.finite_mulSupport_of_discreteTopology {α : Type u_5} [CommGroup α] [TopologicalSpace α] [DiscreteTopology α] {β : Type u_6} (f : β → α) (h : Multipliable f) : (Function.mulSupport f).Finite

theorem Summable.finite_support_of_discreteTopology {α : Type u_5} [AddCommGroup α] [TopologicalSpace α] [DiscreteTopology α] {β : Type u_6} (f : β → α) (h : Summable f) : (Function.support f).Finite

theorem Multipliable.countable_mulSupport {α : Type u_1} {G : Type u_4} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] {f : α → G} [FirstCountableTopology G] [T1Space G] (hf : Multipliable f) : (Function.mulSupport f).Countable

theorem Summable.countable_support {α : Type u_1} {G : Type u_4} [TopologicalSpace G] [AddCommGroup G] [IsTopologicalAddGroup G] {f : α → G} [FirstCountableTopology G] [T1Space G] (hf : Summable f) : (Function.support f).Countable

theorem multipliable_const_iff {β : Type u_2} {G : Type u_4} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [Infinite β] [T2Space G] (a : G) : (Multipliable fun (x : β) => a) ↔ a = 1

theorem summable_const_iff {β : Type u_2} {G : Type u_4} [TopologicalSpace G] [AddCommGroup G] [IsTopologicalAddGroup G] [Infinite β] [T2Space G] (a : G) : (Summable fun (x : β) => a) ↔ a = 0

@[simp]

theorem tprod_const {β : Type u_2} {G : Type u_4} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T2Space G] (a : G) : ∏' (x : β), a = a ^ Nat.card β

@[simp]

theorem tsum_const {β : Type u_2} {G : Type u_4} [TopologicalSpace G] [AddCommGroup G] [IsTopologicalAddGroup G] [T2Space G] (a : G) : ∑' (x : β), a = Nat.card β • a

Groups with a zero

These lemmas apply to a CommGroupWithZero; the most familiar case is when K is a field. These are specific to the product setting and do not have a sensible additive analogue.

theorem HasProd.congr_cofinite₀ {α : Type u_1} {K : Type u_4} [CommGroupWithZero K] [TopologicalSpace K] [ContinuousMul K] {f g : α → K} {c : K} (hc : HasProd f c) {s : Finset α} (hs : ∀ a ∈ s, f a ≠ 0) (hs' : ∀ a ∉ s, f a = g a) : HasProd g (c * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i))

theorem Multipliable.tsum_congr_cofinite₀ {α : Type u_1} {K : Type u_4} [CommGroupWithZero K] [TopologicalSpace K] [ContinuousMul K] {f g : α → K} [T2Space K] (hc : Multipliable f) {s : Finset α} (hs : ∀ a ∈ s, f a ≠ 0) (hs' : ∀ a ∉ s, f a = g a) : ∏' (i : α), g i = (∏' (i : α), f i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)

@[deprecated Multipliable.tsum_congr_cofinite₀ (since := "2025-04-12")]

theorem tsum_congr_cofinite {α : Type u_1} {K : Type u_4} [CommGroupWithZero K] [TopologicalSpace K] [ContinuousMul K] {f g : α → K} [T2Space K] (hc : Multipliable f) {s : Finset α} (hs : ∀ a ∈ s, f a ≠ 0) (hs' : ∀ a ∉ s, f a = g a) : ∏' (i : α), g i = (∏' (i : α), f i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)

Alias of Multipliable.tsum_congr_cofinite₀.

theorem Multipliable.congr_cofinite₀ {α : Type u_1} {K : Type u_4} [CommGroupWithZero K] [TopologicalSpace K] [ContinuousMul K] {f g : α → K} (hf : Multipliable f) (hf' : ∀ (a : α), f a ≠ 0) (hfg : ∀ᶠ (a : α) in Filter.cofinite, f a = g a) : Multipliable g

See also Multipliable.congr_cofinite, which does not have a non-vanishing condition, but instead requires the target to be a group under multiplication (and hence fails for infinite products in a ring).