Summable if partial sums tend to zero

Stream: Is there code for X?

[Xavier Roblot]

I am looking for a statement that says that f : ℕ → ℝ is summable iff the partial sum $\sum_{i=n}^m f_i$ tends to zero whenever $n, m \to \infty$. I am not even sure on how to state it:

import Mathlib

example (f : ℕ → ℝ) :
    Tendsto (fun (n, m) ↦ ∑ k in Finset.Ico n m, f k) atTop (𝓝 0) ↔ Summable f := by
  sorry

example (f : ℕ → ℝ) :
    ∀ m, Tendsto (fun n ↦ ∑ k in Finset.Ico n (n + m), f k) atTop (𝓝 0) ↔ Summable f := by
  sorry

We have some close results with Finset but I really need to have interval instead.

[Sébastien Gouëzel]

Are you sure this is true? If you take 1, then -1, then 1/2, then -1/2, then 1/3, then -1/3 and so on, then the sequence is not summable, but the partial sums along intervals tend to zero if I'm not mistaken.

[Kevin Buzzard]

Yeah, "summable" in Lean means "absolutely convergent" for sequences of reals.

[Xavier Roblot]

Yeah, I see. That might be a problem for what I want to prove...

[Jireh Loreaux]

If your series is nonnegative, then checking intervals would be sufficient. But otherwise, docs#summable_iff_vanishing_norm is the best you can do.

[Xavier Roblot]

Let me #xy for you so you see what the problem is. Consider a : ℕ → ℂ and assume that $\sum_{n \le t} a_n$ is in $O(t^r)$ for some $r$. Then the Dirichlet series $\sum_{n \geq 1} a_n/ n^ s$ converges for $\Re(s) > r$. This is proved in Marcus, Number Fields, p. 129 and the way to prove it is to estimate the partial sums $\sum_{k=n}^m a_n/n^s$ and prove that they tends to zero whenever $n, m \to +\infty$.

[Xavier Roblot]

So I guess, unless a : ℕ → ℝ≥0, I don't get absolute convergence and thus I have to assume that if I want to have docs#LSeriesSummable

[Kevin Buzzard]

Surely you mean something like Re(s)>r or something? If a_n=n then the sum is O(t^2) but this is zeta(s+1). (edit: now fixed)

Do you care about convergence which isn't absolute? e.g. are you summing Dirichlet series with nontrivial characters and 0<Re(s)<1 for example? Do these sums converge to functions which are holomorphic in s? (showing my ignorance of what happens beyond Re(s)=1)

[Xavier Roblot]

Right. Sorry. Let me fix that.

[Kevin Buzzard]

Concrete maths question to make my ignorance clear: the sum $1/1^s-1/2^s+1/3^s-1/4^s+\cdots$ converges absolutely for $s\in\mathbb{C}$ with Re(s)>1 to a holomorphic function (n^s is defined to be exp(s.log(n)) for n a positive integer so there's no branch cuts involved). It also converges, non-absolutely, for Re(s)>0. Presumably the sum is still holomorphic as a function of s but I've realised I'm not entirely sure why.

[Xavier Roblot]

I am far from an expert on this topic. I am trying to formalize the result at https://mathoverflow.net/questions/482347/residue-of-dirichlet-series-at-s-1 (second answer) and I need summability to make things works...

[Xavier Roblot]

And I don't know how to get it...

[Mitchell Lee]

Kevin Buzzard said:

Concrete maths question to make my ignorance clear: the sum $1/1^s-1/2^s+1/3^s-1/4^s+\cdots$ converges absolutely for $s\in\mathbb{C}$ with Re(s)>1 to a holomorphic function (n^s is defined to be exp(s.log(n)) for n a positive integer so there's no branch cuts involved). It also converges, non-absolutely, for Re(s)>0. Presumably the sum is still holomorphic as a function of s but I've realised I'm not entirely sure why.

I don't know a counterexample off the top of my head, but I don't think absolute convergence is enough to imply that a series of holomorphic functions is holomorphic. However, locally uniform convergence is sufficient (https://proofwiki.org/wiki/Uniform_Limit_of_Analytic_Functions_is_Analytic). You can do that particular sum for Re(s) > 0 by pairing adjacent summands to get

$$\sum_{n = 1}^\infty \left(\frac{1}{(2n - 1)^s} - \frac{1}{(2n)^s}\right),$$

which is absolutely and locally uniformly convergent on {Re(s) > 0}.

[Mitchell Lee]

Conditional convergence for series tends to be written out explicitly in mathlib. So the equation

$$\sum_{n = 0}^\infty f(n) = L$$

would be written simply as HasSum f L if the series is unconditionally convergent, but it would need to be written as Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds L) if the series is only conditionally convergent. For example, see HasSum.tendsto_sum_nat. This should probably be considered a gap in the library.

[Michael Stoll]

For L-series, it is generally true that if it converges (conditionally) at some point $s_0$, then it is holomorphic on the half-plane $\Re s > \Re s_0$. However, this is not available in Mathlib (yet), basically because of Mathlib's equating convergence with absolute convergence.

[Michael Stoll]

It would make sense to develop some theory and API for conditionally converging series (at least when the domain of summation is Nat, but possibly in larger generality, if it makes sense).

[Michael Stoll]

@Xavier Roblot Are you thinking of Dedekind zeta functions? Maybe @David Loeffler has some ideas how to prove analytic continuation for them.

[Mitchell Lee]

Conditionally convergent series can be defined for functions on a locally finite preorder; I am not sure if this is the correct amount of generality.

[Yakov Pechersky]

If you phrase is using cofinite instead of atTop, does that help with generality?

[Xavier Roblot]

Michael Stoll said:

Xavier Roblot Are you thinking of Dedekind zeta functions? Maybe David Loeffler has some ideas how to prove analytic continuation for them.

Well, I need the result I quoted above for the analytic class number formula. Of course, in this case, the coefficients are Nat, so conditional convergence and absolute convergence are the same. Still, since I had to formalize the result I wanted to prove it in the most general version (the one given on MathOverflow) and for that I need to prove the L-series is summable for $\Re(s) > r$ when its coefficients satisfies $\sum_{n \le t} a_n$ is in $O(t^r)$ which is not true in general. So I'll have to prove a weaker version.

[Michael Stoll]

Maybe you can state the result in such a way that it refers to a function that is complex differentiable on some right half-plane and agrees with the L-series on the (possibly smaller) half-plane where it converges absolutely? (With a special case lemma when both are the same). Then your result can be used in its intended generality when somebody adds results on conditional convergence of L-series at some later point.

[Mitchell Lee]

Mitchell Lee said:

Conditionally convergent series can be defined for functions on a locally finite preorder; I am not sure if this is the correct amount of generality.

Explicitly:

import Mathlib

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

[Xavier Roblot]

Michael Stoll said:

Maybe you can state the result in such a way that it refers to a function that is complex differentiable on some right half-plane and agrees with the L-series on the (possibly smaller) half-plane where it converges absolutely? (With a special case lemma when both are the same). Then your result can be used in its intended generality when somebody adds results on conditional convergence of L-series at some later point.

Yes, that may be the best solution

[David Loeffler]

Alternatively, maybe it might make sense to work with the hypothesis that $\sum_{n \le t} |a_n| = O(t^r)$? This would still cover Xavier's intended use case.

[David Loeffler]

By the way, I feel I should issue a public apology here. Several weeks ago I reviewed one of Xavier PR's (intended as part of a chain of PR's leading to the analytic class number formula), and expressed the view that some results about convergence of L-series were being done in too specific a way, and should be formulated more generally. It seems that the generalisation is far, far harder and more involved than I realised.

Xavier: please allow me to offer my sincere apologies for all the extra work I have imposed on you!

[Xavier Roblot]

@David Loeffler , don’t worry about that! That’s actually what I like the most about Mathlib development: starting on some proof and on the way finding yourself working on something else totally different. I have discovered a lot of parts of Mathlib very different from my domain this way and learned a lot.

[Xavier Roblot]

And it’s fun too