Analysis: series

[lowasser]

I'm getting back to this and trying to build a good definition for series.

Wikipedia uses the term "series" to refer only to infinite sums, and I buy that. I also claim that there's really no useful notion of series without a corresponding notion of convergence.

So what exactly is the setting in which a series is defined? A commutative monoid with a metric space? We don't necessarily have to be quite so general, but I'd at least like something general enough to encompass real and complex numbers, and maybe even some other handy spaces.

If we were in the habit of using standard topologies instead of metric spaces, we might define it over a topological group? I don't know. Ideas welcome. I could also just start the ungeneralized version, sticking to real numbers, but that'd feel very out of character for this project.

[fredrik-bakke]

I'll likely have some more thought-out input on this later, but for now I can recommend checking out the concept of "closeness spaces" as considered in Todd Ambride's thesis Exact Real Search: Formalised Optimisation and Regression in Constructive Univalent Mathematics. These seem like a promising setting in which to study convergence of series constructively. In particular, they should at times allow you to avoid principles of omniscience, although I do not have sufficient experience in this area to make a definitive statement. If you should choose to use this concept, I have the compactness of the extended natural numbers formalized in some unmerged branch (currently blocked on #1264 #1387).

[lowasser]

I have to admit I'm not yet convinced that we need -- at least, anytime soon -- something specialized to constructive settings, at least for the problem I'm describing here. The scope of this issue is intended to enclose only "in what settings can you define convergence of a series at all."

(The constructive setting places lots of constraints on how you can show convergence -- no monotone convergence, you have to lean much harder on Cauchy conditions -- but that's a separate problem that we're making lots of progress on with Bernoulli's inequality and the like.)

At this point, my default is to construct, like, Ab-With-Metric or some other combined structure.

[fredrik-bakke]

Ah, I see, I misunderstood your question the first time around. My bad

[lowasser]

Or, reframed: we already have metric spaces and lots of infrastructure for defining convergence there, and I believe that'll suffice for our near term needs. I'm just starting to skim the thesis you linked, but I think it's strictly more sophisticated than we need to get analysis and some basic functions defined.