Smooth Urysohn Lemma

Stream: PrimeNumberTheorem+

[Bolton Bailey]

I think I remember this one from my undergrad topology course, isn't the answer $e^{1/x}$ or something?
Is it a free-for-all on the lemmas or is there some sort of permission we need to get started on this/are we waiting on something?

[Terence Tao]

Bolton Bailey said:

I think I remember this one from my undergrad topology course, isn't the answer $e^{1/x}$ or something?
Is it a free-for-all on the lemmas or is there some sort of permission we need to get started on this/are we waiting on something?

We should soon make a regular status announcement (like we did for PFR, e.g., at https://leanprover.zulipchat.com/#narrow/stream/412902-Polynomial-Freiman-Ruzsa-conjecture/topic/Outstanding.20tasks.2C.20version.208.2E0 ) to formally announce the tasks that people might volunteer to work on, but it may take a little time to get everything organized. In the meantime, if anyone wants to claim a lemma to work on right away, please feel free to announce doing so in this thread, and we will try to keep track of everything as it happens. In particular, smooth Urysohn is definitely up for grabs right now!

The lemmas in Section 2 of the blueprint (Wiener-Ikehara Tauberian theorem) have already been formalized at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/PrimeNumberTheoremAnd/Wiener.lean , so they "just" need proofs; I just submitted a PR that will hopefully link up the lean code with the blueprint and create a number of blue bubbles that people can start working on. Over the next few days I plan to do something similar with Section 5 (Elementary corollaries). Maybe Alex can chime in on what the status is on the other sections right now.

[Yury G. Kudryashov]

We have smooth partition of unity (and smooth bump functions as a dependency) in Mathlib.

[Yury G. Kudryashov]

See docs#exists_smooth_zero_one_of_isClosed for Urysohns-like statement.

[Bolton Bailey]

Ok, well, I now have a sorry-free statement of the smooth Urysohn lemma from the project using Yury's function, I'll PR that but feel free to ignore it if someone has come up with something better.

[Bolton Bailey]

Seems I need permission to PR directly by publishing a branch. Should I make a separate fork / can permission be granted to GitHub user BoltonBailey?

[Alex Kontorovich]

Bolton Bailey said:

Seems I need permission to PR directly by publishing a branch. Should I make a separate fork / can permission be granted to GitHub user BoltonBailey?

I just added you as a collaborator. But others were able to PR without needing this step, so I'm not sure why you weren't able to PR?... Thanks!

[Bolton Bailey]

It still says
Screenshot-2024-01-31-at-2.26.34-PM.png

[Rémy Degenne]

You could do what is suggested on that picture: create a fork, work on it, then once your work is done create a PR to the main repository from the fork. I see that there are several PRs merged from forks already.

[Bolton Bailey]

Yeah, happy to do that if that's the workflow, but I am asking if that is the right way. I guess the answer is "yes"?

[Bolton Bailey]

Ok I see now that maybe the issue was that I needed to accept the invitation.

[Bolton Bailey]

Ok I have made a PR. I have also made another one for the SmoothExistence stub.

[Yury G. Kudryashov]

What version is needed for the project? Possibly, we have something closer to that in Mathlib.

[Alex Kontorovich]

Yury G. Kudryashov said:

What version is needed for the project? Possibly, we have something closer to that in Mathlib.

I think you're asking about this line, right?

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"@"e659b1b"

Of course at some point we might want to update it to a later version of Mathlib (hopefully without breaking too much...)?

[Yury G. Kudryashov]

I meant "what version of the statement", not "what version of Mathlib". Sorry for confusion.

[Alex Kontorovich]

Ah, I see. @Bolton Bailey already did the version we need! I'm working on compiling a list of "next low hanging fruit"... Coming soon...