Zulip Chat Archive

Stream: new members

Topic: Contribution possibilities

Harald Krämer (Nov 01 2023 at 19:52):


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 (Nov 01 2023 at 19:54):

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

Patrick Massot (Nov 01 2023 at 19:59):

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 (Nov 01 2023 at 19:59):

Does it make sense?

Harald Krämer (Nov 01 2023 at 20:04):

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 (Nov 01 2023 at 20:05):

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 ff is non-increasing and goes to zero at infinity. Then there exists ll such that the series n(1)nfn\sum_n (-1)^nf_n converges to ll.

Patrick Massot (Nov 01 2023 at 20:06):

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 (Nov 01 2023 at 20:06):

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

Harald Krämer (Nov 01 2023 at 20:09):

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 (Nov 01 2023 at 20:09):

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 (Nov 01 2023 at 20:10):

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

Harald Krämer (Nov 01 2023 at 20:15):

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 (Nov 01 2023 at 20:19):

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 (Nov 01 2023 at 20:20):

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

Last updated: Dec 20 2023 at 11:08 UTC