Summable, and multiple instance parameters

Stream: new members

[Philippe Duchon]

I tried browsing the Mathlib documentation, checking to see if things I might want to use are there (and indeed they typically are), and found the Summable predicate (in Mathlib.Topology.Algebra.InfiniteSum.Defs), and related constructions/properties.

Basically, Summable is part of what I was looking for: it states that some family of elements of a topological "space" has an unconditional sum.

What surprised me are the instance parameters associated with the definition: [AddCommMonoid a] and [TopologicalSpace a]. My understanding is that this says that we have both a commutative monoid and a topological space with carrier set a (not sure how to type the Greek letters into Zulip, this is supposed to be an alpha), but it doesn't seem to impose any compatibility conditions on the two structures (like, a TopologicalSemiring is a semiring where addition and multiplication are continuous). Is there some subtle relationship between the two that I am missing in the definitions, or is that because at this point the definitions don't require any conditions and these come later in the theory? (This may very well come from a misunderstanding on my part of how instance parameters work)

Also (and this is more related to the way Mathlib is built), I see this part of the library deals with infinite sums indexed over a whole type, and defines its notations for them. But does the library also have infinite sums indexed by a set (that is, add in a predicate for membership in the set into the notation)? Of course these would reduce to sums indexed by the whole type by mapping values not in the set to 0 (possibly with some added automation in proofs).

[Daniel Weber]

You can look at the implementation notes:

We say that a function f : β → α has an unconditional product of a if the function fun s : [Finset](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Finset/Basic.html#Finset) β ↦ ∏ b ∈ s, f b converges to a on the atTop filter on [Finset](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Finset/Basic.html#Finset) β. In other words, for every neighborhood U of a, there exists a finite set s : [Finset](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Finset/Basic.html#Finset) β of indices such that ∏ b ∈ s', f b ∈ U for any finite set s' which is a superset of s.

In particular, no relation between the topological space and the monoid is needed for the definition

[Eric Wieser]

Philippe Duchon said:

But does the library also have infinite sums indexed by a set

This can be handled by treating the set as a type (ie, pairs of elements and proofs that they belong to the set)

Of course these would reduce to sums indexed by the whole type by mapping values not in the set to 0 (possibly with some added automation in proofs).

docs#tsum_subtype is the statement of this result.

[Philippe Duchon]

Thanks, this shows I still have a lot of work before I can semi-fluently read the docs...

[Kevin Buzzard]

I was stunned once to notice the observation you're making, that there was no compatibility between the topology and addition in the definition and the first few theorems. The point is that all the theorems proved in the Defs file (and the beginning of the Basic file) are really trivial. Here is the point in the exposition where the group law is assumed to be continuous with respect to the topology. The first theorem proved after that is (the multiplicative version of) sum of the limit is the limit of the sums, for two sequences.