# Infinite sums and products in topological groups #

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

source
theorem HasProd.inv {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} {a : α} (h : HasProd f a L) :
HasProd (fun (b : β) => (f b)⁻¹) a⁻¹ L
source
theorem HasSum.neg {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} {a : α} (h : HasSum f a L) :
HasSum (fun (b : β) => -f b) (-a) L
source
theorem Multipliable.inv {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} (hf : Multipliable f L) :
Multipliable (fun (b : β) => (f b)⁻¹) L
source
theorem Summable.neg {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} (hf : Summable f L) :
Summable (fun (b : β) => -f b) L
source
theorem Multipliable.of_inv {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} (hf : Multipliable (fun (b : β) => (f b)⁻¹) L) :
Multipliable f L
source
theorem Summable.of_neg {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} (hf : Summable (fun (b : β) => -f b) L) :
Summable f L
source
theorem multipliable_inv_iff {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} :
Multipliable (fun (b : β) => (f b)⁻¹) L ↔ Multipliable f L
source
theorem summable_neg_iff {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} :
Summable (fun (b : β) => -f b) L ↔ Summable f L
source
theorem HasProd.div {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f g : β → α} {a₁ a₂ : α} (hf : HasProd f a₁ L) (hg : HasProd g a₂ L) :
HasProd (fun (b : β) => f b / g b) (a₁ / a₂) L
source
theorem HasSum.sub {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f g : β → α} {a₁ a₂ : α} (hf : HasSum f a₁ L) (hg : HasSum g a₂ L) :
HasSum (fun (b : β) => f b - g b) (a₁ - a₂) L
source
theorem Multipliable.div {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f g : β → α} (hf : Multipliable f L) (hg : Multipliable g L) :
Multipliable (fun (b : β) => f b / g b) L
source
theorem Summable.sub {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f g : β → α} (hf : Summable f L) (hg : Summable g L) :
Summable (fun (b : β) => f b - g b) L
source
theorem Multipliable.trans_div {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f g : β → α} (hg : Multipliable g L) (hfg : Multipliable (fun (b : β) => f b / g b) L) :
Multipliable f L
source
theorem Summable.trans_sub {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f g : β → α} (hg : Summable g L) (hfg : Summable (fun (b : β) => f b - g b) L) :
Summable f L
source
theorem multipliable_iff_of_multipliable_div {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f g : β → α} (hfg : Multipliable (fun (b : β) => f b / g b) L) :
Multipliable f L ↔ Multipliable g L
source
theorem summable_iff_of_summable_sub {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f g : β → α} (hfg : Summable (fun (b : β) => f b - g b) L) :
Summable f L ↔ Summable g L
source
theorem HasProd.update {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} {a₁ : α} [L.LeAtTop] (hf : HasProd f a₁ L) (b : β) [DecidableEq β] (a : α) :
HasProd (Function.update f b a) (a / f b * a₁) L
source
theorem HasSum.update {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} {a₁ : α} [L.LeAtTop] (hf : HasSum f a₁ L) (b : β) [DecidableEq β] (a : α) :
HasSum (Function.update f b a) (a - f b + a₁) L
source
theorem Multipliable.update {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} [L.LeAtTop] (hf : Multipliable f L) (b : β) [DecidableEq β] (a : α) :
Multipliable (Function.update f b a) L
source
theorem Summable.update {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} [L.LeAtTop] (hf : Summable f L) (b : β) [DecidableEq β] (a : α) :
Summable (Function.update f b a) L
source
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₂)
source
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₂)
source
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₁)
source
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₁)
source
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
source
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
source
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)
source
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)
source
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)
source
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)
source
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
source
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
source
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
source
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
source
theorem hasProd_ite_div_hasProd {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} {a : α} [L.LeAtTop] [DecidableEq β] (hf : HasProd f a L) (b : β) :
HasProd (fun (n : β) => if n = b then 1 else f n) (a / f b) L
source
theorem hasSum_ite_sub_hasSum {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} {a : α} [L.LeAtTop] [DecidableEq β] (hf : HasSum f a L) (b : β) :
HasSum (fun (n : β) => if n = b then 0 else f n) (a - f b) L
source
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.

source
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.

source
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.

source
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.

source
theorem Multipliable.congr_atTop {α : Type u_1} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f₁ g₁ : ℕ → α} (hf : Multipliable f₁) (hfg : f₁ =ᶠ[Filter.atTop] g₁) :
Multipliable g₁
source
theorem Summable.congr_atTop {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f₁ g₁ : ℕ → α} (hf : Summable f₁) (hfg : f₁ =ᶠ[Filter.atTop] g₁) :
Summable g₁
source
theorem multipliable_congr_atTop {α : Type u_1} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f₁ g₁ : ℕ → α} (hfg : f₁ =ᶠ[Filter.atTop] g₁) :
Multipliable f₁ ↔ Multipliable g₁
source
theorem summable_congr_atTop {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f₁ g₁ : ℕ → α} (hfg : f₁ =ᶠ[Filter.atTop] g₁) :
Summable f₁ ↔ Summable g₁
source
theorem tprod_inv {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f : β → α} [T2Space α] :
∏'[L] (b : β), (f b)⁻¹ = (∏'[L] (b : β), f b)⁻¹
source
theorem tsum_neg {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f : β → α} [T2Space α] :
∑'[L] (b : β), -f b = -∑'[L] (b : β), f b
source
theorem Multipliable.tprod_div {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [CommGroup α] [TopologicalSpace α] [IsTopologicalGroup α] {f g : β → α} [T2Space α] [L.NeBot] (hf : Multipliable f L) (hg : Multipliable g L) :
∏'[L] (b : β), f b / g b = (∏'[L] (b : β), f b) / ∏'[L] (b : β), g b
source
theorem Summable.tsum_sub {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] {f g : β → α} [T2Space α] [L.NeBot] (hf : Summable f L) (hg : Summable g L) :
∑'[L] (b : β), (f b - g b) = ∑'[L] (b : β), f b - ∑'[L] (b : β), g b
source
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
source
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
source
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.

source
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.

source
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

source
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

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem Multipliable.mulIndicator {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] {f : β → α} [CompleteSpace α] (hf : Multipliable f) (s : Set β) :
Multipliable (s.mulIndicator f)
source
theorem Summable.indicator {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] {f : β → α} [CompleteSpace α] (hf : Summable f) (s : Set β) :
Summable (s.indicator f)
source
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)
source
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)
source
theorem Multipliable.subtype {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [IsUniformGroup α] {f : β → α} [CompleteSpace α] (hf : Multipliable f) (s : Set β) :
Multipliable (f ∘ Subtype.val)
source
theorem Summable.subtype {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] {f : β → α} [CompleteSpace α] (hf : Summable f) (s : Set β) :
Summable (f ∘ Subtype.val)
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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.

source
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.

source
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`.

source
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`.

source
theorem Multipliable.finite_mulSupport_of_discreteTopology {α : Type u_5} [CommGroup α] [TopologicalSpace α] [DiscreteTopology α] {β : Type u_6} (f : β → α) (h : Multipliable f) :
(Function.mulSupport f).Finite
source
theorem Summable.finite_support_of_discreteTopology {α : Type u_5} [AddCommGroup α] [TopologicalSpace α] [DiscreteTopology α] {β : Type u_6} (f : β → α) (h : Summable f) :
(Function.support f).Finite
source
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
source
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
source
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
source
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
source
@[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 β
source
@[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.

source
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))
source
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)
source
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).