Documentation

Mathlib.Topology.Algebra.InfiniteSum.Group

Infinite sums and products in topological groups #

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

theorem HasSum.neg {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} {a : α} (h : HasSum f a) :
HasSum (fun (b : β) => -f b) (-a)
theorem HasProd.inv {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} {a : α} (h : HasProd f a) :
HasProd (fun (b : β) => (f b)⁻¹) a⁻¹
theorem Summable.neg {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} (hf : Summable f) :
Summable fun (b : β) => -f b
theorem Multipliable.inv {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} (hf : Multipliable f) :
Multipliable fun (b : β) => (f b)⁻¹
theorem Summable.of_neg {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} (hf : Summable fun (b : β) => -f b) :
theorem Multipliable.of_inv {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} (hf : Multipliable fun (b : β) => (f b)⁻¹) :
theorem summable_neg_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} :
(Summable fun (b : β) => -f b) Summable f
theorem multipliable_inv_iff {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} :
(Multipliable fun (b : β) => (f b)⁻¹) Multipliable f
theorem HasSum.sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} {g : βα} {a₁ : α} {a₂ : α} (hf : HasSum f a₁) (hg : HasSum g a₂) :
HasSum (fun (b : β) => f b - g b) (a₁ - a₂)
theorem HasProd.div {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} {g : βα} {a₁ : α} {a₂ : α} (hf : HasProd f a₁) (hg : HasProd g a₂) :
HasProd (fun (b : β) => f b / g b) (a₁ / a₂)
theorem Summable.sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} {g : βα} (hf : Summable f) (hg : Summable g) :
Summable fun (b : β) => f b - g b
theorem Multipliable.div {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} {g : βα} (hf : Multipliable f) (hg : Multipliable g) :
Multipliable fun (b : β) => f b / g b
theorem Summable.trans_sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} {g : βα} (hg : Summable g) (hfg : Summable fun (b : β) => f b - g b) :
theorem Multipliable.trans_div {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} {g : βα} (hg : Multipliable g) (hfg : Multipliable fun (b : β) => f b / g b) :
theorem summable_iff_of_summable_sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} {g : βα} (hfg : Summable fun (b : β) => f b - g b) :
theorem multipliable_iff_of_multipliable_div {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} {g : βα} (hfg : Multipliable fun (b : β) => f b / g b) :
theorem HasSum.update {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} {a₁ : α} (hf : HasSum f a₁) (b : β) [DecidableEq β] (a : α) :
HasSum (Function.update f b a) (a - f b + a₁)
theorem HasProd.update {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} {a₁ : α} (hf : HasProd f a₁) (b : β) [DecidableEq β] (a : α) :
HasProd (Function.update f b a) (a / f b * a₁)
theorem Summable.update {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} (hf : Summable f) (b : β) [DecidableEq β] (a : α) :
theorem Multipliable.update {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} (hf : Multipliable f) (b : β) [DecidableEq β] (a : α) :
theorem HasSum.hasSum_compl_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} {a₁ : α} {a₂ : α} {s : Set β} (hf : HasSum (f Subtype.val) a₁) :
HasSum (f Subtype.val) a₂ HasSum f (a₁ + a₂)
theorem HasProd.hasProd_compl_iff {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} {a₁ : α} {a₂ : α} {s : Set β} (hf : HasProd (f Subtype.val) a₁) :
HasProd (f Subtype.val) a₂ HasProd f (a₁ * a₂)
theorem HasSum.hasSum_iff_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} {a₁ : α} {a₂ : α} {s : Set β} (hf : HasSum (f Subtype.val) a₁) :
HasSum f a₂ HasSum (f Subtype.val) (a₂ - a₁)
theorem HasProd.hasProd_iff_compl {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} {a₁ : α} {a₂ : α} {s : Set β} (hf : HasProd (f Subtype.val) a₁) :
HasProd f a₂ HasProd (f Subtype.val) (a₂ / a₁)
abbrev Summable.summable_compl_iff.match_2 {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] {f : βα} (motive : Summable fProp) :
∀ (x : Summable f), (∀ (w : α) (ha : HasSum f w), motive )motive x
Equations
  • =
Instances For
    theorem Summable.summable_compl_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} {s : Set β} (hf : Summable (f Subtype.val)) :
    Summable (f Subtype.val) Summable f
    abbrev Summable.summable_compl_iff.match_1 {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] {f : βα} {s : Set β} (motive : Summable (f Subtype.val)Prop) :
    ∀ (x : Summable (f Subtype.val)), (∀ (w : α) (ha : HasSum (f Subtype.val) w), motive )motive x
    Equations
    • =
    Instances For
      theorem Multipliable.multipliable_compl_iff {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} {s : Set β} (hf : Multipliable (f Subtype.val)) :
      Multipliable (f Subtype.val) Multipliable f
      theorem Finset.hasSum_compl_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} {a : α} (s : Finset β) :
      HasSum (fun (x : { x : β // xs }) => f x) a HasSum f (a + is, f i)
      theorem Finset.hasProd_compl_iff {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} {a : α} (s : Finset β) :
      HasProd (fun (x : { x : β // xs }) => f x) a HasProd f (a * is, f i)
      theorem Finset.hasSum_iff_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} {a : α} (s : Finset β) :
      HasSum f a HasSum (fun (x : { x : β // xs }) => f x) (a - is, f i)
      theorem Finset.hasProd_iff_compl {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} {a : α} (s : Finset β) :
      HasProd f a HasProd (fun (x : { x : β // xs }) => f x) (a / is, f i)
      theorem Finset.summable_compl_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} (s : Finset β) :
      (Summable fun (x : { x : β // xs }) => f x) Summable f
      theorem Finset.multipliable_compl_iff {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} (s : Finset β) :
      (Multipliable fun (x : { x : β // xs }) => f x) Multipliable f
      theorem Set.Finite.summable_compl_iff {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} {s : Set β} (hs : s.Finite) :
      Summable (f Subtype.val) Summable f
      theorem Set.Finite.multipliable_compl_iff {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} {s : Set β} (hs : s.Finite) :
      Multipliable (f Subtype.val) Multipliable f
      theorem hasSum_ite_sub_hasSum {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} {a : α} [DecidableEq β] (hf : HasSum f a) (b : β) :
      HasSum (fun (n : β) => if n = b then 0 else f n) (a - f b)
      theorem hasProd_ite_div_hasProd {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} {a : α} [DecidableEq β] (hf : HasProd f a) (b : β) :
      HasProd (fun (n : β) => if n = b then 1 else f n) (a / f b)
      theorem tsum_neg {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} [T2Space α] :
      ∑' (b : β), -f b = -∑' (b : β), f b
      theorem tprod_inv {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} [T2Space α] :
      ∏' (b : β), (f b)⁻¹ = (∏' (b : β), f b)⁻¹
      theorem tsum_sub {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} {g : βα} [T2Space α] (hf : Summable f) (hg : Summable g) :
      ∑' (b : β), (f b - g b) = ∑' (b : β), f b - ∑' (b : β), g b
      theorem tprod_div {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} {g : βα} [T2Space α] (hf : Multipliable f) (hg : Multipliable g) :
      ∏' (b : β), f b / g b = (∏' (b : β), f b) / ∏' (b : β), g b
      theorem sum_add_tsum_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : βα} [T2Space α] {s : Finset β} (hf : Summable f) :
      xs, f x + ∑' (x : (s)), f x = ∑' (x : β), f x
      theorem prod_mul_tprod_compl {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {f : βα} [T2Space α] {s : Finset β} (hf : Multipliable f) :
      (xs, f x) * ∏' (x : (s)), f x = ∏' (x : β), f x
      theorem tsum_eq_add_tsum_ite {α : Type u_1} {β : Type u_2} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {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.

      theorem tprod_eq_mul_tprod_ite {α : Type u_1} {β : Type u_2} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α] {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_iff_cauchySeq_finset {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [CompleteSpace α] {f : βα} :
      Summable f CauchySeq fun (s : Finset β) => bs, f b

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

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

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

      theorem cauchySeq_finset_iff_sum_vanishing {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : βα} :
      (CauchySeq fun (s : Finset β) => bs, f b) enhds 0, ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t sbt, f b e
      theorem cauchySeq_finset_iff_prod_vanishing {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [UniformGroup α] {f : βα} :
      (CauchySeq fun (s : Finset β) => bs, f b) enhds 1, ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t sbt, f b e
      theorem cauchySeq_finset_iff_tsum_vanishing {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : βα} :
      (CauchySeq fun (s : Finset β) => bs, f b) enhds 0, ∃ (s : Finset β), ∀ (t : Set β), Disjoint t s∑' (b : t), f b e
      theorem cauchySeq_finset_iff_tprod_vanishing {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [UniformGroup α] {f : βα} :
      (CauchySeq fun (s : Finset β) => bs, f b) enhds 1, ∃ (s : Finset β), ∀ (t : Set β), Disjoint t s∏' (b : t), f b e
      theorem summable_iff_vanishing {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : βα} [CompleteSpace α] :
      Summable f enhds 0, ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t sbt, f b e
      theorem multipliable_iff_vanishing {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [UniformGroup α] {f : βα} [CompleteSpace α] :
      Multipliable f enhds 1, ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t sbt, f b e
      theorem summable_iff_tsum_vanishing {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : βα} [CompleteSpace α] :
      Summable f enhds 0, ∃ (s : Finset β), ∀ (t : Set β), Disjoint t s∑' (b : t), f b e
      theorem multipliable_iff_tprod_vanishing {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [UniformGroup α] {f : βα} [CompleteSpace α] :
      Multipliable f enhds 1, ∃ (s : Finset β), ∀ (t : Set β), Disjoint t s∏' (b : t), f b e
      abbrev Summable.summable_of_eq_zero_or_self.match_1 {α : Type u_2} {β : Type u_1} [AddCommGroup α] {f : βα} (e : Set α) (motive : (∃ (s : Finset β), ∀ (t : Finset β), Disjoint t sbt, f b e)Prop) :
      ∀ (x : ∃ (s : Finset β), ∀ (t : Finset β), Disjoint t sbt, f b e), (∀ (s : Finset β) (hs : ∀ (t : Finset β), Disjoint t sbt, f b e), motive )motive x
      Equations
      • =
      Instances For
        theorem Summable.summable_of_eq_zero_or_self {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : βα} {g : βα} [CompleteSpace α] (hf : Summable f) (h : ∀ (b : β), g b = 0 g b = f b) :
        theorem Multipliable.multipliable_of_eq_one_or_self {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [UniformGroup α] {f : βα} {g : βα} [CompleteSpace α] (hf : Multipliable f) (h : ∀ (b : β), g b = 1 g b = f b) :
        theorem Summable.indicator {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : βα} [CompleteSpace α] (hf : Summable f) (s : Set β) :
        Summable (s.indicator f)
        theorem Multipliable.mulIndicator {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [UniformGroup α] {f : βα} [CompleteSpace α] (hf : Multipliable f) (s : Set β) :
        Multipliable (s.mulIndicator f)
        theorem Summable.comp_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : βα} [CompleteSpace α] {i : γβ} (hf : Summable f) (hi : Function.Injective i) :
        theorem Multipliable.comp_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommGroup α] [UniformSpace α] [UniformGroup α] {f : βα} [CompleteSpace α] {i : γβ} (hf : Multipliable f) (hi : Function.Injective i) :
        theorem Summable.subtype {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : βα} [CompleteSpace α] (hf : Summable f) (s : Set β) :
        Summable (f Subtype.val)
        theorem Multipliable.subtype {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [UniformGroup α] {f : βα} [CompleteSpace α] (hf : Multipliable f) (s : Set β) :
        Multipliable (f Subtype.val)
        theorem summable_subtype_and_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : βα} [CompleteSpace α] {s : Set β} :
        ((Summable fun (x : s) => f x) Summable fun (x : s) => f x) Summable f
        theorem multipliable_subtype_and_compl {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [UniformGroup α] {f : βα} [CompleteSpace α] {s : Set β} :
        ((Multipliable fun (x : s) => f x) Multipliable fun (x : s) => f x) Multipliable f
        theorem tsum_subtype_add_tsum_subtype_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] [T2Space α] {f : βα} (hf : Summable f) (s : Set β) :
        ∑' (x : s), f x + ∑' (x : s), f x = ∑' (x : β), f x
        theorem tprod_subtype_mul_tprod_subtype_compl {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [UniformGroup α] [CompleteSpace α] [T2Space α] {f : βα} (hf : Multipliable f) (s : Set β) :
        (∏' (x : s), f x) * ∏' (x : s), f x = ∏' (x : β), f x
        theorem sum_add_tsum_subtype_compl {α : Type u_1} {β : Type u_2} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] [T2Space α] {f : βα} (hf : Summable f) (s : Finset β) :
        xs, f x + ∑' (x : { x : β // xs }), f x = ∑' (x : β), f x
        theorem prod_mul_tprod_subtype_compl {α : Type u_1} {β : Type u_2} [CommGroup α] [UniformSpace α] [UniformGroup α] [CompleteSpace α] [T2Space α] {f : βα} (hf : Multipliable f) (s : Finset β) :
        (xs, f x) * ∏' (x : { x : β // xs }), f x = ∏' (x : β), f x
        theorem Summable.vanishing {α : Type u_1} {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] {f : αG} (hf : Summable f) ⦃e : Set G (he : e nhds 0) :
        ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t skt, f k e
        theorem Multipliable.vanishing {α : Type u_1} {G : Type u_5} [TopologicalSpace G] [CommGroup G] [TopologicalGroup G] {f : αG} (hf : Multipliable f) ⦃e : Set G (he : e nhds 1) :
        ∃ (s : Finset α), ∀ (t : Finset α), Disjoint t skt, f k e
        theorem Summable.tsum_vanishing {α : Type u_1} {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup 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 Multipliable.tprod_vanishing {α : Type u_1} {G : Type u_5} [TopologicalSpace G] [CommGroup G] [TopologicalGroup 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 tendsto_tsum_compl_atTop_zero {α : Type u_1} {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] (f : αG) :
        Filter.Tendsto (fun (s : Finset α) => ∑' (a : { x : α // xs }), 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 tendsto_tprod_compl_atTop_one {α : Type u_1} {G : Type u_5} [TopologicalSpace G] [CommGroup G] [TopologicalGroup G] (f : αG) :
        Filter.Tendsto (fun (s : Finset α) => ∏' (a : { x : α // xs }), 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 Summable.tendsto_cofinite_zero {α : Type u_1} {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup 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.tendsto_cofinite_one {α : Type u_1} {G : Type u_5} [TopologicalSpace G] [CommGroup G] [TopologicalGroup 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.countable_support {α : Type u_1} {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] {f : αG} [FirstCountableTopology G] [T1Space G] (hf : Summable f) :
        (Function.support f).Countable
        theorem summable_const_iff {β : Type u_2} {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] [Infinite β] [T2Space G] (a : G) :
        (Summable fun (x : β) => a) a = 0
        theorem multipliable_const_iff {β : Type u_2} {G : Type u_5} [TopologicalSpace G] [CommGroup G] [TopologicalGroup G] [Infinite β] [T2Space G] (a : G) :
        (Multipliable fun (x : β) => a) a = 1
        @[simp]
        theorem tsum_const {β : Type u_2} {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] [T2Space G] (a : G) :
        ∑' (x : β), a = Nat.card β a
        @[simp]
        theorem tprod_const {β : Type u_2} {G : Type u_5} [TopologicalSpace G] [CommGroup G] [TopologicalGroup G] [T2Space G] (a : G) :
        ∏' (x : β), a = a ^ Nat.card β