Conditionally convergent series

Stream: mathlib4

[Mitchell Lee]

Today there was a discussion about conditionally convergent series in this thread: #Is there code for X? > Summable if partial sums tend to zero.

Perhaps it is time to add conditionally convergent series to mathlib. My proposal is something like the following:

import Mathlib

open Filter
def HasConditionalSum {α β : Type*} [Preorder β] [LocallyFiniteOrder β]
    [AddCommMonoid α] [TopologicalSpace α] (f : β → α) (a : α) : Prop :=
  Tendsto (fun ⟨l, u⟩ ↦ ∑ i ∈ Finset.Icc l u, f i)
    (atBot ×ˢ atTop) (nhds a)

In words, if $\beta$ is a type with a locally finite preorder, then we say that a sum $\sum_{b \in \beta} f(b)$ converges conditionally to $a$ if the finite partial sums $\sum_{\ell \leq b \leq u} f(b)$ converge to $a$ as the lower bound $\ell$ approaches the bottom and the upper bound $u$ approaches the top. If $\beta = \mathbb{N}$, then this is equivalent to the statement that

$$\lim_{n \to \infty} \left(\sum_{i = 0}^{n - 1} f(i)\right) = a,$$

which is already written out in full in mathlib in a few places (for example, HasSum.tendsto_sum_nat).

Then, we can define ConditionallySummable and ctsum as the conditional analogues of Summable and tsum. Similarly, we may define conditionally multipliable products.

(One could argue that it is slightly inelegant to have both ctsum and tsum, because unconditional summability implies conditional summability to the same value, but I don't see an easy way around it.)

Any thoughts? One specific question I have is what the notation for ctsum should be.

[Yury G. Kudryashov]

Why this is the preferred definition, e.g., for Int?

[Yury G. Kudryashov]

The competing definition for Int involves sums over symmetric intervals. Note: I never needed conditionally convergent series indexed by something other than Nat.

[Yury G. Kudryashov]

But the symmetric definition is similar to https://en.wikipedia.org/wiki/Cauchy_principal_value for integrals.

[Kevin Buzzard]

For naturals we genuinely seem to have a situation coming from arithmetic where people care about a convergent series which doesn't converge absolutely (it is some generalization of the Riemann zeta function like $1/1^s-1/3^s+1/5^s-1/7^s+\cdots$ and $0<s<1$). Do we have some analogous situation for the integers?

[Mitchell Lee]

For Int, if $\alpha$ is complete and T3, then it's equivalent to the statement that the sum on the nonnegative values of $b$ and the sum on the negative values of $b$ both have partial sums which converge. I am not sure if we would prefer to have sums over symmetric intervals though.

[Mitchell Lee]

Probably T3 is not necessary, actually.

[Yury G. Kudryashov]

A possible approach is to define this notion for α = Nat only.

[Mitchell Lee]

I'm not sure. Maybe I am just trying to make things more general than they really need to be.

[Mitchell Lee]

I have been searching for some references that define series indexed over sets over than $\mathbb{N}$. It seems the usual definition over $\mathbb{Z}$ is the one that requires both the series over the positive and the negative integers to converge; e.g. https://ncatlab.org/nlab/show/doubly+infinite+series.

I also found some definitions of double series $\sum_{m, n = 0}^\infty a_{m, n}$ that require the rectangular partial sums to converge: https://encyclopediaofmath.org/wiki/Double_series

I don't know in what situation these concepts are useful, though.

[Eric Wieser]

(Note that LocallyFiniteOrder.finsetIcc is an implementation detail, the correct spelling is Finset.Icc)

[Mitchell Lee]

The same definition of series over $\mathbb{N} \times \mathbb{N}$ also appears in Apostol's Mathematical Analysis
apostol.PNG

I'm still not sure of a situation in which it is important to consider conditionally convergent series on domains other than $\mathbb{N}$, but it at least seems like the definition involving sums over intervals is the "correct" definition.

[Kevin Buzzard]

@David Loeffler or @Chris Birkbeck do either of you know precisely what the definition of the presumably not absolutely convergent sum over the integers defining the generalized modular form $E_2$ is? Is the idea to immediately rewrite as a sum over the naturals?

[Mitchell Lee]

One other remark: most authors use the term "conditionally summable" to mean "summable, but not unconditionally summable", so maybe we should use names other than HasConditionalSum and ConditionallySummable, but I don't know what would be best.

[Luigi Massacci]

Mitchell Lee said:

I'm still not sure of a situation in which it is important to consider conditionally convergent series on domains other than $\mathbb{N}$, but it at least seems like the definition involving sums over intervals is the "correct" definition.

Trigonometric series?

[Mitchell Lee]

Good point. Your comment has reminded me of sinc interpolation (https://en.wikipedia.org/wiki/Whittaker%E2%80%93Shannon_interpolation_formula) which is going to be a conditionally convergent series on $\mathbb{Z}$ if the signal is constant.

[David Loeffler]

Kevin Buzzard said:

David Loeffler or Chris Birkbeck do either of you know precisely what the definition of the presumably not absolutely convergent sum over the integers defining the generalized modular form $E_2$ is? Is the idea to immediately rewrite as a sum over the naturals?

$E_2$ is kind of a non-example here, because the whole point -- the thing that makes $E_2$ interesting -- is precisely that there isn't a uniquely defined notion of conditionally-convergent sum over $\mathbb{Z}^2$. If I remember correctly, it is defined by an expression of the form
$\lim_{X \to \infty} \left(\sum_{\substack{m \in \mathbb{Z} \\ |m| \le X}} \left( \lim_{Y \to \infty} \sum_{\substack{n \in \mathbb{Z} \\ |n| \le Y}} a_{mn} \right)\right)$
and if you take the limit over $X, Y$ in the opposite order you get a genuinely different value.

[Chris Birkbeck]

Kevin Buzzard said:

David Loeffler or Chris Birkbeck do either of you know precisely what the definition of the presumably not absolutely convergent sum over the integers defining the generalized modular form $E_2$ is? Is the idea to immediately rewrite as a sum over the naturals?

So for G_2 I've been experimenting with using this as the definition

def G₂ : ℍ → ℂ := fun z =>  limUnder (atTop)
    (fun N : ℕ => ∑ m in Finset.Icc (-N : ℤ) N, (∑' (n : ℤ), 1 / ((m : ℂ) * z + n) ^ 2))

(although it might end up being a Ico in the sum to make some proof easier). But yes, writing it as a sum over the natural seems so far , form what I've seen, to be the easiest thing to work with. That said, I think more API for conditionally convergent series is definitely welcome! and its quite possible that the defn I've been experimenting with is not the best!

[David Loeffler]

I think the $E_2$ example maybe doesn't tell us much about the "right" notion for $\mathbb{Z}^2$, but does add further evidence that for sums over $\mathbb{Z}$ the "right" notion is some sort of (approximately) symmetric-interval limit, summing over over Icc (-N) N or maybe Ico (-N) N etc as $N \to \infty$.

I believe that is also the usual notion of conditional summability over $\mathbb{Z}$ in Fourier theory, see e.g. Dirichlet-Jordan convergence test on Wikipedia.

[Mitchell Lee]

I agree that the notion of symmetric partial sums converging is very useful and should appear in mathlib somewhere, but I am not convinced that it should be the definition of convergent $\mathbb{Z}$-indexed sums.

[Mitchell Lee]

I think it would be nice to have one definition of convergence that could work in the same way for $\mathbb{N}$ and $\mathbb{Z}$ and $\mathbb{N} \times \mathbb{N}$, so we could prove theorems about all sums on all these index sets using the same API. Then, later on, we could define the "principal value" of a $\mathbb{Z}$-indexed series based on the symmetric partial sums.

[Mitchell Lee]

If we want to express both $\mathbb{N}$-indexed series and principal values of $\mathbb{Z}$-indexed series, we're going to need two definitions regardless. So I think we may as well do it in such a way that the definition for $\mathbb{N}$-indexed series also gives a reasonable answer for other index types.

[David Loeffler]

Mitchell Lee said:

If we want to express both $\mathbb{N}$-indexed series and principal values of $\mathbb{Z}$-indexed series, we're going to need two definitions regardless. So I think we may as well do it in such a way that the definition for $\mathbb{N}$-indexed series also gives a reasonable answer for other index types.

Certainly, it does no harm if the definition we use for $\mathbb{N}$ also gives something meaningful for other types. But I'm not convinced by the definition you're proposing, using atBot ×ˢ atTop. It seems to me that you are making the $\mathbb{N}$ case more complicated than necessary for (what seems to me) rather little gain, because it looks like the only other interesting type you get this way is $\mathbb{Z}$, and for that case it gives a notion of summability that doesn't match the one that's natural in applications. I'd be inclined to define HasConditionalSum for a LocallyFiniteOrderBot instead, using a sum over Iic or Iio.

Is there a succinct way of spelling out "a type with a norm such that all balls { |x| < N } are finite"?

[Mitchell Lee]

There are at least some sources (like nlab) who say that a $\mathbb{Z}$-indexed series converges if the positive and negative end both do. Also, it seems like most texts on complex analysis agree that this is what is meant when a Laurent series is said to converge. (I concede that this doesn't matter that much because Laurent series are usually only considered when they converge absolutely, but I would also hesitate to say that it doesn't matter at all.) In a complete topological group, this is equivalent to the statement that the interval sums converge on atBot ×ˢ atTop. So, this definition is at least useful for something when applied to $\mathbb{Z}$, even if that "something" is just matching the literature more closely.

Also, the definition of $\mathbb{Z}$-indexed series that uses sums over symmetric intervals is poorly behaved in some unfortunate ways, so I think it would be a shame to have only that definition. For example, it's possible for the series $\sum_{n \in \mathbb{Z}} f(n)$ and $\sum_{n \in \mathbb{Z}} f(n + 1)$ to both converge in that sense, but have different values.

On a LocallyFiniteOrderBot, the definition you propose using Iic is equivalent to the one that uses atBot ×ˢ atTop, because atBot = pure ⊥. I think this is easy enough to prove that it is really not a big deal.

[Johan Commelin]

David Loeffler said:

Is there a succinct way of spelling out "a type with a norm such that all balls { |x| < N } are finite"?

Sounds like some sort of pointed discrete metric space? But I'm not sure we have a nice spelling for that in mathlib already...

[Mitchell Lee]

(Unimportant sidenote: here are the nlab definition and the definition I am proposing, for series indexed by $\mathbb{Z}$.

• $\sum_{n \in \mathbb{Z}} f(n) = a$ means that $\sum_{n = 0}^\infty f(n) + \sum_{n = 1}^{\infty} f(-n) = a$
• $\sum_{n \in \mathbb{Z}} f(n) = a$ means that $\lim_{(\ell, u) \to (-\infty, \infty)}\sum_{\ell \leq n \leq u} f(n) = a$

As mentioned, these two definitions are equivalent if the sum takes place in a complete topological group. But for general topological groups, the latter definition is weaker; for example, it allows $\sum_{n \in \mathbb{Z} \setminus \{0\}} \frac{1}{n^3} = 0$ even if the sum is carried out in $\mathbb{Q}$. It is also better behaved because it allows pulling back sums along inducing homomorphisms; i.e. a theorem similar to docs#Topology.IsInducing.hasSum_iff.)

[David Loeffler]

I would be wary of basing too much on that nLab page (analysis is not really nLab's focus, to say the least).

But all the proposed definitions agree in the obviously-most-important case of sums over $\mathbb{N}$; so let's not let this debate hold up progress on that. If you are prepared to take on the task of coding up a prototype implementation, and the (very minor) extra effort of rewriting away the atBot in the case of sums over $\mathbb{N}$ doesn't trouble you, then you have my grateful encouragement to go ahead with your proposed definition

[Johan Commelin]

It also does the right thing for $\N \times \N$ right? Or does that need more thought?

[Mitchell Lee]

Thank you. Do you have any suggestion for the name? I don't want to call it HasConditionalSum and ConditionallySummable because "conditionally summable" implies not being unconditionally summable, but maybe there is no better option.

[David Loeffler]

Johan Commelin said:

It also does the right thing for $\N \times \N$ right? Or does that need more thought?

My view is that for just about any type other than $\mathbb{N}$, there is not a unique Right Thing. But Mitchell's definition is definitely a sensible definition in this case.

[Mitchell Lee]

Apostol's Mathematical Analysis and Encyclopedia of Mathematics both define $\mathbb{N} \times \mathbb{N}$-indexed series using rectangular partial sums. I agree that there are other sensible definitions though.

[David Loeffler]

Mitchell Lee said:

Thank you. Do you have any suggestion for the name? I don't want to call it HasConditionalSum and ConditionallySummable because "conditionally summable" implies not being unconditionally summable, but maybe there is no better option.

I think HasConditionalSum / ConditionallySummable is fine; or we could go with a shortening of that (HasCondSum / CondSummable)?

[Mitchell Lee]

I'll try it with the shortening

[Mitchell Lee]

Do we want ctsum or just csum? Also, what should be the notation for the sums?

[Mitchell Lee]

(I must admit I don't know what the t in tsum stands for, so I don't have very much intuition for this.)

[David Loeffler]

tsum is "topological sum" I think. So ctsum seems sensible. For notation, how about ∑ᶜ?

[Mitchell Lee]

(I would like to just change the definition of tsum so that it returns the correct value if the series is either unconditionally convergent or conditionally convergent, but I don't think that's possible because conditional convergence requires a typeclass assumption, and this would break some existing theorems that rely on the fact that tsum returns a junk value of 0 for series that are not unconditionally convergent.)

[Mitchell Lee]

Yeah, I'll try ∑ᶜ.

[Mario Carneiro]

I think the right generalization of conditionally convergent series takes a filter on the index type

[Mario Carneiro]

in fact, that might even generalize tsum itself, since there is a canonical choice of filter which just uses all finite sets ordered by inclusion

[David Loeffler]

@Mario Carneiro what is the definition you have in mind?

[Mario Carneiro]

rather than using all finite sets, you can use all initial segments of Nat to obtain the usual notion of conditionally convergent series on nat

[Mario Carneiro]

the definition is otherwise very similar to tsum

[David Loeffler]

Just to be precise, we're not actually talking about filters on the index type, but filters on finsets on the index type, right?

[Mario Carneiro]

it's actually a very simple generalization. Before:

def HasProd (f : β → α) (a : α) : Prop :=
  Tendsto (fun s : Finset β ↦ ∏ b ∈ s, f b) atTop (𝓝 a)

After:

def HasFilterProd (L : Filter (Finset β)) (f : β → α) (a : α) : Prop :=
  Tendsto (fun s : Finset β ↦ ∏ b ∈ s, f b) L (𝓝 a)

[Johan Commelin]

Hah! I like the look of that. I guess we could even move L last, and give it a default value?
Or is that asking for pain?

[Mario Carneiro]

I think it would be best to keep it separate, inspired by the design at docs#HasFDerivAtFilter

[Mitchell Lee]

Perhaps I will look through all the theorems about HasProd and see which ones can be deduced from more general statements about HasFilterProd

[Mario Carneiro]

is there a snappy name or way to obtain the filter of initial segments of nat?

[Mitchell Lee]

I think it's Filter.map Finset.range atTop

[Johan Commelin]

I guess it's also nhds 0?

[Johan Commelin]

Aah, but only the finite nhds...

[Mario Carneiro]

I don't think so, it would have to be nhds of a finset

[Mario Carneiro]

and I don't think nhds {} gives the right result (it's just pure {} because the topology of Finset Nat is not interesting)

[Mario Carneiro]

you have to somehow get the order structure of nat involved

[David Loeffler]

I really like Mario's suggestion here, because all of the rival suggestions that were proposed for sums over $\mathbb{Z}$, $\mathbb{N} \times \mathbb{N}$ etc are all obtainable as special cases in a completely transparent way. Chapeau, as the French say!

[Johan Commelin]

Mario Carneiro said:

I don't think so, it would have to be nhds of a finset

Yeah, I got my thinking confused.

[Yury G. Kudryashov]

Mitchell Lee said:

I think it's Filter.map Finset.range atTop

Or Filter.map Finset.Iic .atTop, if we want it to work in any locally finite order with bot.

[Ruben Van de Velde]

Filters save the day again

[Jireh Loreaux]

Personally, I think it would be nice to keep the ∑' notation for the usual atTop specialization fo the new definition. It would be annoying to have to specify the filter all the time when using that.

[Xavier Roblot]

I guess ∑ᶠ could be a good notation for the new definition.

[David Loeffler]

Xavier Roblot said:

I guess ∑ᶠ could be a good notation for the new definition.

That already means something else, doesn't it? Sums with finite support, IIRC?

[Xavier Roblot]

Too bad...

[Yury G. Kudryashov]

We can have ∑' i, a i and ∑'[f] i, a i.

[Jireh Loreaux]

I worry about that notation when the filter f is many characters, but I don't have an alternative to suggest.

[Yury G. Kudryashov]

∑' i along f, a i?

[Jireh Loreaux]

I think that's better than having delimiters separated by many characters. Although does that mean we have to make along a keyword? My understanding of macros is still poor.

[Yury G. Kudryashov]

∑' i in f, a i would be misleading, because f is a filter on Finset ι, not ι.

[Jireh Loreaux]

indeed.

[Mitchell Lee]

Okay, I am convinced that the definition involving a filter of sets on Finset is the right generalization. Thanks Mario. (It also lets you do sums like $\sum_{n = 5}^\infty f(n)$, which might be nice. And I guess you could technically do $\sum_{m = 0}^\infty \sum_{n = 0}^\infty f(m, n)$ as a single sum on $\mathbb{N} \times \mathbb{N}$ using this, but I don't know if you would want to do that.)

I like the notation ∑'[f] i, a i. If you defined the filters cond and pv correctly, you could then write ∑'[cond] i, a i for usual conditional convergence and ∑'[pv] i, a i for principal value of a sum on $\mathbb{Z}$, which I think looks pretty nice. I agree that it could get messy if you needed longer names, though.

[Mitchell Lee]

I am getting somewhat distracted by other things; I can start working on a PR for this in a few days, but I would be happy if someone else did it before then.

[Yury G. Kudryashov]

Mitchell Lee said:

And I guess you could technically do $\sum_{m = 0}^\infty \sum_{n = 0}^\infty f(m, n)$ as a single sum on $\mathbb{N} \times \mathbb{N}$ using this, but I don't know if you would want to do that.)

I think that docs#Filter.curry gives this (haven't checked).