Riemann series theorem?

Stream: Is there code for X?

[Niels Voss]

Is there a proof of the Riemann series theorem (also called the Riemann rearrangement theorem) in Lean? I tried looking around in mathlib's infinite sum API but if I understand this correctly, it seemed that most sums were of the form

$$\lim_{S \text{ becomes a larger and larger finite subset of X}} \sum_{t \in S}t$$

so I couldn't find much on series defined as the limit of partial sums. My understanding (and I might be wrong) is that mathlib's definition only works for series that converge absolutely.

More generally, is there any easier way to work with these types of series other than something like filter.tendsto (λ k, (finset.range k).sum f) filter.at_top (nhds c). Alternatively, how do you work with conditionally convergent series?

[Eric Wieser]

Can you write the lean statement you're looking for?

[Niels Voss]

This wasn't actually for an existing project, I was just interested in knowing if anyone had tried this yet.
My best attempt at recreating this in a Lean statement was (and this might be totally wrong):

import data.real.basic
import topology.algebra.infinite_sum.basic
import topology.instances.real
import analysis.normed.group.basic

def converges (series : ℕ → ℝ) : Prop := ∃ c : ℝ, filter.tendsto (λ k, (finset.range k).sum series) filter.at_top (nhds c)
def converges_absolutely (series : ℕ → ℝ) : Prop := converges (λ n, ‖(series n)‖)

theorem riemann_rearrangement_theorem {series : ℕ → ℝ} (h₁ : converges series)
  (h₂ : ¬converges_absolutely series) (C : ℝ) : ∃ (p : ℕ → ℕ), function.bijective p ∧
    filter.tendsto (λ k, (finset.range k).sum (λ n, series (p n))) filter.at_top (nhds C) := sorry

I haven't really checked this because I'm somewhat unfamiliar with how limits in Lean work in general

[Yaël Dillies]

@Yakov Pechersky, that's a you question :eyes:

[Kevin Buzzard]

Yes, we don't have this kind of sum in lean. I'm not an analyst but my impression is that this concept of summation is just used for undergraduate teaching and is not particularly central any more (summing divergent series used to be a thing but perhaps not so much now)

[Kevin Buzzard]

The lean definition of sum, as you say Niels, is equivalent to "absolutely convergent, and sum is..."

[Yaël Dillies]

Not quite, Kevin, no. It's not absolute convergence that we have in mathlib, but unconditional convergence., which is (slightly) weaker.

[Yakov Pechersky]

I think Yael is right. For an example, I think the alternating harmonic series is summable.

[Kevin Buzzard]

What? Surely not.

[Yakov Pechersky]

Because the partial sums when split out both diverge?

[Kevin Buzzard]

Do absolute and unconditional convergence coincide for nat-indexed sequences of reals? (I have no idea what unconditional convergence is)

[Sebastien Gouezel]

For sequences of reals, yes, they are equivalent. Not in general, though: let e_n be the standard basis of a Hilbert space. Then n -> e_n / n is not absolutely converging, but it is unconditionally converging.

[Sebastien Gouezel]

(i.e., in whatever order you do the summation you will get the same limit).

[Pedro Sánchez Terraf]

Kevin Buzzard said:

Yes, we don't have this kind of sum in lean. I'm not an analyst but my impression is that this concept of summation is just used for undergraduate teaching and is not particularly central any more (summing divergent series used to be a thing but perhaps not so much now)

Not an analyst either, but I seem to recall that “summability methods” were/are used for something, and actually prominent examples of those are based on looking at the summation of the first terms (calibrated by some weight, for instance, Cesàro's).

[Kevin Buzzard]

Right -- Hardy even wrote a book on divergent series. But that was a long time ago.

[Eric Rodriguez]

I find the idea that "this maths isn't trendy anymore" to be a weak explanation for not having certain things. Certainly if the methods have evolved to give the same results, that's nice, but if we miss maths due to the results not being as trendy?

[Reid Barton]

I mean, there is a lot of trendy math that we are missing too (almost all of it in fact).

[Reid Barton]

One has to choose what to do somehow.

[Patrick Massot]

Yes, it's all a matter of priorities. People are welcome to work on numerical series, and this work will get to mathlib at some point after the port.

[Niels Voss]

So, just to confirm, we don't have the Riemann series theorem in Lean and it is generally low priority, but could be added to mathlib after the port or if there is time? I was considering working on it, though I'm not quite sure I know enough to actually prove it.

[Patrick Massot]

I think so.

[Jireh Loreaux]

As an analyst who has done some reasonable amount of work with divergent series I can say that they definitely still matter. At the same time, I completely understand why mathlib has taken an alternate approach and considers these sorts of things low priority.

[Mario Carneiro]

I've always viewed the riemann series theorem as a curiosity or endpoint theorem. It helps you understand the nature of conditionally convergent series but it's not actually all that useful as a building block for other things, is it?

[Julien Puydt]

Riemann series are useful as a reference family to prove the convergence of other series.

[David Loeffler]

@Julien Puydt I think you have misunderstood what this thread is about. (I suspect you are thinking about the convergence of the series defining the Riemann zeta function for $\operatorname{Re}(s) > 1$, which has been in mathlib essentially forever.)

[Julien Puydt]

@David Loeffler indeed ; sorry for the noise!

[Jireh Loreaux]

Mario, I haven't used the Riemann rearrangement theorem explicitly that I recall, but I have definitely seen similar theorems used. For instance, I know an argument that makes use of the following fact: given a divergent series of positive numbers (terms converge to zero though), and any other nonsummable sequence of positive numbers (not necessarily converging to zero), there is a partition of the series such that the sum of each subseries is the corresponding term in the second sequence.

[Jireh Loreaux]

Oh actually I take it back, I think I have used the Riemann rearrangement theorem. I have a paper which shows that an idempotent operator acting on a Hilbert space is not a Hilbert-Schmidt perturbation of a projection if and only if there is an orthonormal basis relative to which the diagonal of the matrix representation of this operator is the zero sequence. I'm fairly certain the forward implication uses this result under the hood somewhere.

[Kevin Buzzard]

Well this has been very enlightening :-) Thanks Jireh! @Niels Voss maybe you want to make a little PR about convergent (in the undergrad sense) series?

[Niels Voss]

I don't have much free time this week, but I can try next week.
Would it be better to keep the definition of a series as nat -> real, or should I define a new type which allows for dot notation (kind of like how matrix defined its own type)? Alternatively I could use seq which allows both finite and infinite series

[Kevin Buzzard]

My instinct is nat -> some topological monoid

[Yaël Dillies]

I would say α → β where locally_finite_order_bot α and topological_ring β.

[Niels Voss]

Aside from the level of generality, should it be defined as something like

def series (R : Type u) [topological_ring R] := nat -> R

Or should there not be any special type for series at all, and nat -> R will be used directly in theorem statements?
I normally think of a series as a special way of interpreting a sequence, and so the latter feels more natural to me, but the former allows dot notation and typeclass instances for series. And I have heard of people studying series as their own type of object as well.

[Yaël Dillies]

I would expect no special type.

[Eric Wieser]

Niels Voss said:

like how matrix defined its own type

This is necessary because matrix multiplication is not function (elementwise) multiplication