Infinite sum and product in a topological monoid

This file defines infinite products and sums for (possibly infinite) indexed families of elements in a commutative topological monoid (resp. add monoid).

To handle convergence questions we use the formalism of summation filters (defined in the file Mathlib.Topology.Algebra.InfiniteSum.SummationFilter). These are filters on the finite subsets of a given type, and we define a function to be summable for a summation filter L if its partial sums over finite subsets tend to a limit along L (and similarly for products).

This simultaneously generalizes several different kinds of summation: for instance, unconditional summation (which makes sense for any index type) where we take the limit with respect to the atTop filter; but also conditional summation for functions on ℕ, where the limit is over the partial sums ∑ i ∈ range n, f i as n → ∞ (so there exist conditionally-summable sequences which are not unconditionally summable).

Implementation notes

We say that a function f : β → α has a product of a w.r.t. the summation filter L if the function fun s : Finset β ↦ ∏ b ∈ s, f b converges to a w.r.t. the filter L.filter on Finset β.

In the most important case of unconditional summation, this translates to the following condition: for every neighborhood U of a, there exists a finite set s : Finset β of indices such that ∏ b ∈ s', f b ∈ U for any finite set s' which is a superset of s.

This may yield some unexpected results. For example, according to this definition, the product ∏' n : ℕ, (1 : ℝ) / 2 unconditionally exists and is equal to 0. More strikingly, the product ∏' n : ℕ, (n : ℝ) unconditionally exists and is equal to 0, because one of its terms is 0 (even though the product of the remaining terms diverges). Users who would prefer that these products be considered not to exist can carry them out in the unit group ℝˣ rather than in ℝ.

References

• Bourbaki: General Topology (1995), Chapter 3 §5 (Infinite sums in commutative groups)

def HasProd {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (f : β → α) (a : α) (L : SummationFilter β := SummationFilter.unconditional β) : Prop

HasProd f a L means that the (potentially infinite) product of the f b for b : β converges to a along the SummationFilter L.

By default L is the unconditional one, corresponding to the limit of all finite sets towards the entire type. So we take the product over bigger and bigger finite sets. This product operation is invariant under permuting the terms (while products for more general summation filters usually are not).

For the definition and many statements, α does not need to be a topological monoid, only a monoid with a topology (i.e. the multiplication is not assumed to be continuous). We only add this assumption later, for the lemmas where it is relevant.

These are defined in an identical way to infinite sums (HasSum). For example, we say that the function ℕ → ℝ sending n to 1 / 2 has a product of 0, rather than saying that it does not converge as some authors would.

Equations

• HasProd f a L = Filter.Tendsto (fun (s : Finset β) => ∏ b ∈ s, f b) L.filter (nhds a)

def HasSum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) (a : α) (L : SummationFilter β := SummationFilter.unconditional β) : Prop

HasSum f a L means that the (potentially infinite) sum of the f b for b : β converges to a along the SummationFilter `L``.

By default L is the unconditional one, corresponding to the limit of all finite sets towards the entire type. So we take the sum over bigger and bigger finite sets. This sum operation is invariant under permuting the terms (while sums for more general summation filters usually are not). This is based on Mario Carneiro's infinite sum df-tsms in Metamath.

In particular, the function ℕ → ℝ sending n to (-1) ^ n / (n + 1) does not have a sum for this definition, although it is summable for the conditional summation filter that takes limits of sums over n ∈ {0, ..., X} as X → ∞. However, a series which is absolutely convergent with respect to the conditional summation filter is in fact unconditionally summable.

For the definition and many statements, α does not need to be a topological additive monoid, only an additive monoid with a topology (i.e. the addition is not assumed to be continuous). We only add this assumption later, for the lemmas where it is relevant.

Equations

• HasSum f a L = Filter.Tendsto (fun (s : Finset β) => ∑ b ∈ s, f b) L.filter (nhds a)

def Multipliable {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (f : β → α) (L : SummationFilter β := SummationFilter.unconditional β) : Prop

Multipliable f means that f has some (infinite) product with respect to L. Use tprod to get the value.

Equations

• Multipliable f L = ∃ (a : α), HasProd f a L

def Summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) (L : SummationFilter β := SummationFilter.unconditional β) : Prop

Summable f means that f has some (infinite) sum with respect to L. Use tsum to get the value.

Equations

• Summable f L = ∃ (a : α), HasSum f a L

theorem Multipliable.mono_filter {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {L₁ L₂ : SummationFilter β} (hf : Multipliable f L₂) (h : L₁.filter ≤ L₂.filter) : Multipliable f L₁

theorem Summable.mono_filter {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {L₁ L₂ : SummationFilter β} (hf : Summable f L₂) (h : L₁.filter ≤ L₂.filter) : Summable f L₁

@[irreducible]

noncomputable def tprod {α : Type u_4} {β : Type u_5} [CommMonoid α] [TopologicalSpace α] (f : β → α) (L : SummationFilter β := SummationFilter.unconditional β) : α

∏' i, f i is the unconditional product of f, if it exists, or 1 otherwise. ]

More generally, if L is a SummationFilter, ∏'[L] i, f i is the product of f with respect to L if it exists, and 1 otherwise.

(Note that even if the unconditional product exists, it might not be unique if the topology is not separated. When the multiplicative support of f is finite, we make the most reasonable choice, to use the product over the multiplicative support. Otherwise, we choose arbitrarily an a satisfying HasProd f a. Similar remarks apply to more general summation filters.)

Equations

• One or more equations did not get rendered due to their size.

theorem tprod_def {α : Type u_4} {β : Type u_5} [CommMonoid α] [TopologicalSpace α] (f : β → α) (L : SummationFilter β) : tprod f L = if h : Multipliable f L then if L.HasSupport ∧ (Function.mulSupport f ∩ L.support).Finite then finprod (L.support.mulIndicator f) else if HasProd f 1 L then 1 else Exists.choose h else 1

noncomputable def tsum {α : Type u_4} {β : Type u_5} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) (L : SummationFilter β := SummationFilter.unconditional β) : α

∑' i, f i is the unconditional sum of f if it exists, or 0 otherwise.

More generally, if L is a SummationFilter, ∑'[L] i, f i is the sum of f with respect to L if it exists, and 1 otherwise.

(Note that even if the unconditional sum exists, it might not be unique if the topology is not separated. When the support of f is finite, we make the most reasonable choice, to use the sum over the support. Otherwise, we choose arbitrarily an a satisfying HasSum f a. Similar remarks apply to more general summation filters.)

Equations

• tsum f L = if h : Summable f L then if L.HasSupport ∧ (Function.support f ∩ L.support).Finite then finsum (L.support.indicator f) else if HasSum f 0 L then 0 else Exists.choose h else 0

theorem tsum_def {α : Type u_4} {β : Type u_5} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) (L : SummationFilter β) : tsum f L = if h : Summable f L then if L.HasSupport ∧ (Function.support f ∩ L.support).Finite then finsum (L.support.indicator f) else if HasSum f 0 L then 0 else Exists.choose h else 0

∑' i, f i is the unconditional sum of f if it exists, or 0 otherwise.

More generally, if L is a SummationFilter, ∑'[L] i, f i is the sum of f with respect to L if it exists, and 1 otherwise.

(Note that even if the unconditional sum exists, it might not be unique if the topology is not separated. When the support of f is finite, we make the most reasonable choice, to use the sum over the support. Otherwise, we choose arbitrarily an a satisfying HasSum f a. Similar remarks apply to more general summation filters.)

def «term∏'[_]_,_» : Lean.ParserDescr

∏' i, f i is the unconditional product of f, if it exists, or 1 otherwise. ]

More generally, if L is a SummationFilter, ∏'[L] i, f i is the product of f with respect to L if it exists, and 1 otherwise.

(Note that even if the unconditional product exists, it might not be unique if the topology is not separated. When the multiplicative support of f is finite, we make the most reasonable choice, to use the product over the multiplicative support. Otherwise, we choose arbitrarily an a satisfying HasProd f a. Similar remarks apply to more general summation filters.)

Equations

• One or more equations did not get rendered due to their size.

def «term∑'[_]_,_» : Lean.ParserDescr

∑' i, f i is the unconditional sum of f if it exists, or 0 otherwise.

More generally, if L is a SummationFilter, ∑'[L] i, f i is the sum of f with respect to L if it exists, and 1 otherwise.

(Note that even if the unconditional sum exists, it might not be unique if the topology is not separated. When the support of f is finite, we make the most reasonable choice, to use the sum over the support. Otherwise, we choose arbitrarily an a satisfying HasSum f a. Similar remarks apply to more general summation filters.)

Equations

• One or more equations did not get rendered due to their size.

def «term∏'_,_» : Lean.ParserDescr

∏' i, f i is the unconditional product of f, if it exists, or 1 otherwise. ]

More generally, if L is a SummationFilter, ∏'[L] i, f i is the product of f with respect to L if it exists, and 1 otherwise.

(Note that even if the unconditional product exists, it might not be unique if the topology is not separated. When the multiplicative support of f is finite, we make the most reasonable choice, to use the product over the multiplicative support. Otherwise, we choose arbitrarily an a satisfying HasProd f a. Similar remarks apply to more general summation filters.)

Equations

• One or more equations did not get rendered due to their size.

def «term∑'_,_» : Lean.ParserDescr

∑' i, f i is the unconditional sum of f if it exists, or 0 otherwise.

More generally, if L is a SummationFilter, ∑'[L] i, f i is the sum of f with respect to L if it exists, and 1 otherwise.

(Note that even if the unconditional sum exists, it might not be unique if the topology is not separated. When the support of f is finite, we make the most reasonable choice, to use the sum over the support. Otherwise, we choose arbitrarily an a satisfying HasSum f a. Similar remarks apply to more general summation filters.)

Equations

• One or more equations did not get rendered due to their size.

theorem hasProd_bot {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} (hL : ¬L.NeBot) (f : β → α) (a : α) : HasProd f a L

theorem hasSum_bot {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} (hL : ¬L.NeBot) (f : β → α) (a : α) : HasSum f a L

theorem multipliable_bot {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} (hL : ¬L.NeBot) (f : β → α) : Multipliable f L

theorem summable_bot {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} (hL : ¬L.NeBot) (f : β → α) : Summable f L

theorem tprod_bot {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} (hL : ¬L.NeBot) (f : β → α) : ∏'[L] (b : β), f b = ∏ᶠ (b : β), f b

If the summation filter is the trivial filter ⊥, then the topological product is equal to the finite product (which is taken to be 1 if the multiplicative support of f is infinite).

Note that in this case HasProd f a is satisfied for every element a of the target, so the value assigned to the tprod is a question of conventions.

theorem tsum_bot {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} (hL : ¬L.NeBot) (f : β → α) : ∑'[L] (b : β), f b = ∑ᶠ (b : β), f b

If the summation filter is the trivial filter ⊥, then the topological sum is equal to the finite sum (which is taken to be 1 if the support of f is infinite).

Note that in this case HasSum f a is satisfied for every element a of the target, so the value assigned to the tsum is a question of conventions.

theorem HasProd.multipliable {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {a : α} (h : HasProd f a L) : Multipliable f L

theorem HasSum.summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {a : α} (h : HasSum f a L) : Summable f L

theorem tprod_eq_one_of_not_multipliable {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} (h : ¬Multipliable f L) : ∏'[L] (b : β), f b = 1

theorem tsum_eq_zero_of_not_summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} (h : ¬Summable f L) : ∑'[L] (b : β), f b = 0

theorem Function.Injective.hasProd_map_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {L : SummationFilter γ} {g : γ → β} (hg : Injective g) : HasProd f a (L.map { toFun := g, inj' := hg }) ↔ HasProd (f ∘ g) a L

theorem Function.Injective.hasSum_map_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {L : SummationFilter γ} {g : γ → β} (hg : Injective g) : HasSum f a (L.map { toFun := g, inj' := hg }) ↔ HasSum (f ∘ g) a L

theorem Function.Injective.hasProd_comap_iff_of_hasSupport {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {a : α} [L.HasSupport] {g : γ → β} (hg : Injective g) (hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 1) : HasProd (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasProd f a L

theorem Function.Injective.hasSum_comap_iff_of_hasSupport {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {a : α} [L.HasSupport] {g : γ → β} (hg : Injective g) (hf : ∀ x ∈ L.support, x ∉ Set.range g → f x = 0) : HasSum (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasSum f a L

theorem Function.Injective.hasProd_comap_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {a : α} {g : γ → β} (hg : Injective g) (hf : ∀ x ∉ Set.range g, f x = 1) : HasProd (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasProd f a L

theorem Function.Injective.hasSum_comap_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {a : α} {g : γ → β} (hg : Injective g) (hf : ∀ x ∉ Set.range g, f x = 0) : HasSum (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasSum f a L

theorem Function.Injective.hasProd_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → β} (hg : Injective g) (hf : ∀ x ∉ Set.range g, f x = 1) : HasProd (f ∘ g) a ↔ HasProd f a

theorem Function.Injective.hasSum_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → β} (hg : Injective g) (hf : ∀ x ∉ Set.range g, f x = 0) : HasSum (f ∘ g) a ↔ HasSum f a

theorem hasProd_subtype_comap_iff_of_mulSupport_subset {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {a : α} {s : Set β} (hf : Function.mulSupport f ⊆ s) : HasProd (f ∘ Subtype.val) a (L.comap (Function.Embedding.subtype fun (x : β) => x ∈ s)) ↔ HasProd f a L

theorem hasSum_subtype_comap_iff_of_support_subset {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {a : α} {s : Set β} (hf : Function.support f ⊆ s) : HasSum (f ∘ Subtype.val) a (L.comap (Function.Embedding.subtype fun (x : β) => x ∈ s)) ↔ HasSum f a L

theorem hasProd_subtype_iff_of_mulSupport_subset {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {s : Set β} (hf : Function.mulSupport f ⊆ s) : HasProd (f ∘ Subtype.val) a ↔ HasProd f a

theorem hasSum_subtype_iff_of_support_subset {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {s : Set β} (hf : Function.support f ⊆ s) : HasSum (f ∘ Subtype.val) a ↔ HasSum f a

theorem hasProd_fintype_support {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [Fintype β] (f : β → α) (L : SummationFilter β) [L.HasSupport] [DecidablePred fun (x : β) => x ∈ L.support] : HasProd f (∏ b ∈ L.support.toFinset, f b) L

theorem hasSum_fintype_support {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [Fintype β] (f : β → α) (L : SummationFilter β) [L.HasSupport] [DecidablePred fun (x : β) => x ∈ L.support] : HasSum f (∑ b ∈ L.support.toFinset, f b) L

theorem hasProd_fintype {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] [Fintype β] (f : β → α) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] : HasProd f (∏ b : β, f b) L

theorem hasSum_fintype {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [Fintype β] (f : β → α) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] : HasSum f (∑ b : β, f b) L

theorem Finset.hasProd_support {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) (L : SummationFilter ↑↑s := SummationFilter.unconditional ↑↑s) [L.HasSupport] [DecidablePred fun (x : ↑↑s) => x ∈ L.support] : HasProd (f ∘ Subtype.val) (∏ b ∈ map (Function.Embedding.subtype fun (x : β) => x ∈ ↑s) L.support.toFinset, f b) L

theorem Finset.hasSum_support {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) (L : SummationFilter ↑↑s := SummationFilter.unconditional ↑↑s) [L.HasSupport] [DecidablePred fun (x : ↑↑s) => x ∈ L.support] : HasSum (f ∘ Subtype.val) (∑ b ∈ map (Function.Embedding.subtype fun (x : β) => x ∈ ↑s) L.support.toFinset, f b) L

theorem Finset.hasProd {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) (L : SummationFilter ↑↑s := SummationFilter.unconditional ↑↑s) [L.LeAtTop] : HasProd (f ∘ Subtype.val) (∏ b ∈ s, f b) L

theorem Finset.hasSum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) (L : SummationFilter ↑↑s := SummationFilter.unconditional ↑↑s) [L.LeAtTop] : HasSum (f ∘ Subtype.val) (∑ b ∈ s, f b) L

theorem hasProd_prod_support_of_ne_finset_one {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {s : Finset β} (hf : ∀ b ∈ L.support, b ∉ s → f b = 1) [L.HasSupport] [DecidablePred fun (x : β) => x ∈ L.support] : HasProd f (∏ b ∈ (↑s ∩ L.support).toFinset, f b) L

If a function f is 1 outside of a finite set s, then it HasProd ∏ b ∈ s, f b.

theorem hasSum_sum_support_of_ne_finset_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {s : Finset β} (hf : ∀ b ∈ L.support, b ∉ s → f b = 0) [L.HasSupport] [DecidablePred fun (x : β) => x ∈ L.support] : HasSum f (∑ b ∈ (↑s ∩ L.support).toFinset, f b) L

If a function f vanishes outside of a finite set s, then it HasSum ∑ b ∈ s, f b.

theorem hasProd_prod_of_ne_finset_one {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {s : Finset β} (hf : ∀ b ∉ s, f b = 1) [L.LeAtTop] : HasProd f (∏ b ∈ s, f b) L

If a function f is 1 outside of a finite set s, then it HasProd ∏ b ∈ s, f b.

theorem hasSum_sum_of_ne_finset_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {s : Finset β} (hf : ∀ b ∉ s, f b = 0) [L.LeAtTop] : HasSum f (∑ b ∈ s, f b) L

If a function f vanishes outside of a finite set s, then it HasSum ∑ b ∈ s, f b.

theorem multipliable_of_ne_finset_one {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {s : Finset β} (hf : ∀ b ∉ s, f b = 1) [L.HasSupport] : Multipliable f L

theorem summable_of_ne_finset_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {s : Finset β} (hf : ∀ b ∉ s, f b = 0) [L.HasSupport] : Summable f L

theorem Multipliable.hasProd {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} (ha : Multipliable f L) : HasProd f (∏'[L] (b : β), f b) L

theorem Summable.hasSum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} (ha : Summable f L) : HasSum f (∑'[L] (b : β), f b) L

theorem HasProd.unique {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} [T2Space α] [L.NeBot] {a₁ a₂ : α} : HasProd f a₁ L → HasProd f a₂ L → a₁ = a₂

theorem HasSum.unique {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} [T2Space α] [L.NeBot] {a₁ a₂ : α} : HasSum f a₁ L → HasSum f a₂ L → a₁ = a₂

theorem HasProd.tprod_eq {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {a : α} [T2Space α] [L.NeBot] (ha : HasProd f a L) : ∏'[L] (b : β), f b = a

theorem HasSum.tsum_eq {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {a : α} [T2Space α] [L.NeBot] (ha : HasSum f a L) : ∑'[L] (b : β), f b = a

theorem Multipliable.hasProd_iff {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {a : α} [T2Space α] [L.NeBot] (h : Multipliable f L) : HasProd f a L ↔ ∏'[L] (b : β), f b = a

theorem Summable.hasSum_iff {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} {f : β → α} {a : α} [T2Space α] [L.NeBot] (h : Summable f L) : HasSum f a L ↔ ∑'[L] (b : β), f b = a