Contribution possibilities

Stream: new members

[Harald Krämer]

Moin.

I just recently stumbled across mathlib, lean4 and such through a bunch of toots from Terrence Tao, and found the idea quite fascinating. I've been slogging throrgh a few tutorials over the last month or so, and with some experience in programming, it's not that much rougher than math exercises in uni. It's actually more of a fun puzzle than anything.

I've been considering contributing. I've been tutoring back in uni in some analysis courses, some algebra courses, some categorizations, and I have a bunch of experience as a sysadmin and sre (if you're looking for that, in the off-shoot).

I've been kinda looking at infinite series, limits of these, convergence, divergence, altenating divergence, convergence tests. I'm just a bit intimidated, because there is a whole bunch of things called convergence in mathlib, but I'm not sure if it's that convergence of infinite series? I'm not sure if the existing convergences are the whole "for all epsilon, there is an n, such that whatever < espilon" and such. But I'm no mathematician either.

In short, do you have advice there? Would that be a good learning project to pick up upon?

[Patrick Massot]

We have explanations about the relation between convergence in Mathlib and more elementary notions in the topology chapter of #mil.

[Patrick Massot]

More specifically about series, there are two main notions. The notion of summable families make sense for any family of elements in any topological group, and the entry point is https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/InfiniteSum/Basic.html. But this is not what you seem to have in mind where the order of summation is important. Of course you can state that a series converges in the sense that the sequence of partial sums converges since we have the definition of convergence of sequences and the definition of partial sums. But we don't have a definition combining those. You can find some convergence criterion around docs#Antitone.tendsto_alternating_series_of_tendsto_zero for instance.

[Patrick Massot]

Does it make sense?

[Harald Krämer]

It does make sense. I have been looking thorugh mathlib, and I was wondering if the topology-based approach was about 2-3 levels of generelization beyond what I know :)

[Patrick Massot]

For instance you can decipher

variable  {f : ℕ → ℝ}

theorem Antitone.tendsto_alternating_series_of_tendsto_zero (hfa : Antitone f)
    (hf0 : Tendsto f atTop (𝓝 0)) :
    ∃ l, Tendsto (fun n ↦ ∑ i in range (n + 1), (-1) ^ i * f i) atTop (𝓝 l)

to: We are in a context where f denotes a sequence of real numbers. Assume that $f$ is non-increasing and goes to zero at infinity. Then there exists $l$ such that the series $\sum_n (-1)^nf_n$ converges to $l$.

[Patrick Massot]

But you can see the statement does not use the word series, it directly speaks of convergence of the sum up to a fixed natural number.

[Patrick Massot]

Specifically ∑ i in range (n + 1), (-1) ^ i * f i means $\sum_{i=0}^n (-1)^if_i$.

[Harald Krämer]

yes. which, worrries me in two ways: This wouldn't tell us anything about the limit of this series, but at the same time, I am not comfortable with the constructs involved to make a real statement about this series. Let alone, write a formal proof about this.

[Patrick Massot]

Harald Krämer said:

In short, do you have advice there? Would that be a good learning project to pick up upon?

Now let me answer your question. I think it would be nice to have more of those elementary convergence criteria. You can see from https://leanprover-community.github.io/undergrad_todo.html that some elementary stuff seems to be missing (in the Single Variable Real Analysis section of that page).

[Patrick Massot]

In this specific example there is nothing you can tell about the limit if you don't know more about f.

[Harald Krämer]

That's more what I was thinking about. I'd be fine punching in some of the course things I have here, and then we can see how to generalize it.

[Patrick Massot]

If you decide to start of something in particular you should tell us so that we can double-check it is not yet there (sometimes the undergrad TODO webpage is outdated).

[Harald Krämer]

I will. I'll have to take a look at the mathlib context you provided first, though. than you for you time :)