Direct comparison test

Stream: new members

[Alex Nekrasov]

Hello, everyone!
I am learning lean4 for my coursework in university. I want to formalize some theorems from calculus 2 that we had this year. I've been reading mathlib sources for the past few days and decided to come here to ask some questions.
Is direct comparison test for series already in mathlib? If not, then how is it better to formulate its statement? My first attempt lead to this code:

theorem comparison_test {f : ℕ → ℝ} {g : ℕ → ℝ}
  (zero_le_f : ∀ n, 0 ≤ f n) (f_le_g: ∀ n, f n ≤ g n) (gsum: Summable g) : Summable f := sorry

Also is there any connection between Summable and CauSeq? It looks like this definitions are closely related but I couldn't find any theorems using them both.
Thanks in advance.

[Kevin Buzzard]

For real-valued sequences, Summable is the same as "the sum converges absolutely". Regarding Cauchy sequences, is your question a lean question or a mathematical one?

[Alex Nekrasov]

It was more of a lean question, as I thought that Summable is for conditional convergence. Now it makes more sense why I found no connections with CauSeq.
And how to formulate conditional convergence? I suppose that this works:
Tendsto (fun n : ℕ => ∑ i in range n, f i) atTop (𝓝 a)
Are there any theorems that already use such notion? Or definitions for real-values series convergence?

[Michael Stoll]

See also here.

[Kevin Buzzard]

The historical summary is that it seems that it was only a couple of weeks ago that we found a use for this concept in mathlib :-) We have used absolute convergence for years (the definition is that summing over arbitrary finite subsets converges in the sense of filters but it's the same as absolute convergence if the target is the reals).

[Jireh Loreaux]

@Alex Nekrasov see docs#Summable.of_nonneg_of_le for the version of the comparison test we have in Mathlib (i.e., using absolute convergence).

[Jireh Loreaux]

But of course, since the series are nonnegative the conditional and absolute convergence are the same.