Outstanding Tasks, V4

Stream: Carleson

[Floris van Doorn]

It's time for a new list. I added all the remaining lemmas from chapter 7 as new tasks. Take a quick peek of the proof of a lemma to get a feel for task.

There is a CONTRIBUTING file that contains some useful tips. There are some rendering issues with plastex in chapter 7. In these cases consult the blueprint pdf which should be fine.

Tasks (including uncompleted tasks from last post):

L6. :play: (María Inés de Frutos Fernández) Proposition 2.0.3, proven in chapter 6.

26 :check: (Austin Letson) Prove Lemma 5.2.9
49 :check: ( Sébastien Gouëzel ) Prove Lemma 5.1.2 using the Lemmas in Section 5.4. Probably hard.
55 :play: (Michael Rothgang) Prove Lemma 8.0.1 (long)
56 :play: (Michael Rothgang) Prove Proposition 2.0.5 (quite long)
62 :check: (Pietro Monticone) Prove carleson#laverage_le_globalMaximalFunction. Not hard.
63 :check: (Pietro Monticone) Prove carleson#hasStrongType_globalMaximalFunction.
64 :check: (Pietro Monticone) Fill in the four sorries (that are not commented out) in the Defs file
68 :check: (James Sundstrom) Prove Lemma 7.1.3
69 :check: (James Sundstrom) Prove Lemma 7.1.4
70 :check: (Jeremy Tan) Prove Lemma 7.1.5
71 :check: (James Sundstrom) Prove Lemma 7.1.6
72 :check: (James Sundstrom) Prove Lemma 7.2.1
73 :play: (James Sundstrom) Prove Lemma 7.2.2
74 :new: Prove Lemma 7.2.3
76 :new: Prove Lemma 7.3.1
77 :new: Prove Lemma 7.3.2
78 :new: Prove Lemma 7.3.3
79 :check: (Jeremy Tan) Prove Lemma 7.4.1
80 :check: (Joris Roos) Prove Lemma 7.4.2
81 :check: (Floris van Doorn) Prove Lemma 7.4.3
82 :new: Prove Lemma 7.4.4
83 :new: Prove Lemma 7.4.5
84 :new: Prove Lemma 7.4.6
85 :check: (Jeremy Tan) Prove Lemma 7.4.7
86 :check: (Evgenia Karunus) Prove Lemma 7.5.1
87 :new: Prove Lemma 7.5.2
88 :check: (Evgenia Karunus) Prove Lemma 7.5.3
89 :new: Prove Lemma 7.5.4
90 :new: Prove Lemma 7.5.5
91 :check: (Evgenia Karunus) Prove Lemma 7.5.6
92 :new: Prove Lemma 7.5.7
93 :check: (Evgenia Karunus) Prove Lemma 7.5.8
94 :new: Prove Lemma 7.5.9
95 :play: (Evgenia Karunus) Prove Lemma 7.5.10
96 :play: ️(Evgenia Karunus) Prove Lemma 7.5.11
97 :check: (Joris Roos) Prove Lemma 7.6.1
98 :new: Prove Lemma 7.6.2
99 :new: Prove Lemma 7.6.3
100 :check: (Andrew Yang) Prove Lemma 7.6.4
101 :new: Prove Lemma 7.7.1
102 :new: Prove Lemma 7.7.2
103 :new: Prove Lemma 7.7.3
104 :new: Prove Lemma 7.7.4
105 :new: Prove Proposition 2.0.4
106 :check: (Pietro Monticone) Do task 2 of this thread
107 :check: (Pietro Monticone) (depends on 106) Do task 1 of this thread
108 :check: (Pietro Monticone) Do task 3 of this thread
109 :play: (see here) make sure that carleson#hasStrongType_globalMaximalFunction is sorry-free.
110 :check:( Sébastien Gouëzel ) Prove Lemma 5.1.3. This is the last result from chapter 5. Probably tricky, since it combines a lot of results.

[Jeremy Tan]

I already did Task 53 (Lemma 5.5.2) in https://github.com/fpvandoorn/carleson/pull/129

[Jeremy Tan]

https://github.com/fpvandoorn/carleson/pull/136 finishes Lemma 7.1.5

[Floris van Doorn]

Jeremy Tan said:

I already did Task 53 (Lemma 5.5.2) in https://github.com/fpvandoorn/carleson/pull/129

Thanks for the correction. I fixed it now (by marking it complete in V3).

[Evgenia Karunus]

Hi all! I'd like to take up Task 93 (Lemma 7.5.8) :-)

[Floris van Doorn]

Great, noted!

[Evgenia Karunus]

Task 93 is finished (link), thorough PR review would be appreciated!
I'd like to take up Task 91 (Lemma 7.5.6) next.

[Floris van Doorn]

Thanks! I left some comments on your PR.

[Pietro Monticone]

Task 64 is done. I'd like to claim task 63.

[Pietro Monticone]

Updated version of task 63 :check: (PR)

[Andrew Yang]

This looks fun! I'd like to claim task :100:.

[Pietro Monticone]

Task 106 and 107 :check: (PR)

[Pietro Monticone]

Task 108 :check: (PR)

[Michael Rothgang]

To avoid duplicate work: #162 contains an in-progress bump of the project to Mathlib 4.13.0. Help fixing this is welcome; otherwise, I may finish this next week.

[Pietro Monticone]

Unfortunately a previous commit removed doc-gen4 and dependencies from lake-manifest.json. Fixed it.

[Pietro Monticone]

Ok, fixed everything apart from this line.

[Michael Rothgang]

Pietro Monticone said:

Unfortunately a previous commits removed doc-gen4 and dependencies from lake-manifest.json. Fixed it.

Yes, I was unsure about that commit myself. Thanks for confirming that it was bad. And thanks for all the fixes!

[Kevin Buzzard]

See the discussion on the FLT thread about how to decimate your lake-manifest.json and how the FRO don't like the usual fix for this

[Kevin Buzzard]

(sorry on mobile but probably searching for "decimate" will find it)

[Edward van de Meent]

the conversation from this message

[Kim Morrison]

Kevin Buzzard said:

See the discussion on the FLT thread about how to decimate your lake-manifest.json and how the FRO don't like the usual fix for this

I would say rather that it is everyone who keeps getting confused by -R -Kenv=dev that doesn't like the usual fix, and I keep saying "so don't use -R -Kenv=dev then!".

[Kevin Buzzard]

Sorry -- just to be clear -- what I was trying to point out earlier was "Kim suggested a better way to do all of this than -Kenv=dev, involving requiring a separate repo for doc-generation" and Edward has supplied the link (thanks!)

[Michael Rothgang]

I will try to apply the fix suggested there (separate Docs folder with separate lakefile) next week.

[Michael Rothgang]

Pietro Monticone said:

Ok, fixed everything apart from this line.

I think there is more work to it; I got a bit further yesterday. I sorried half a dozen broken proofs; and something w.r.t. finiteness broke. Help with both is still welcome.

[Pietro Monticone]

Fix everything unsorried

[Pietro Monticone]

Now I am going to take a look at the sorried ones

[Pietro Monticone]

Now CI pass, but I am not sure which are all the sorried ones.

[Michael Rothgang]

PR #168 labelled all remaining sorries. I will take a look at them - unless you beat me to it :-)

[Pietro Monticone]

Thank you @Michael Rothgang, but I don't think I'll be able to find the time this week.

[Evgenia Karunus]

I'd like to take on Task 86 (Lemma 7.5.1).

[Austin Letson]

I created a PR for 5.2.9: https://github.com/fpvandoorn/carleson/pull/183

[Pietro Monticone]

Task 62 :check: (PR)

[Jeremy Tan]

Sorry for the long break @Floris van Doorn… I have (as of a few minutes before this post, 2024-11-22T11:00:00+08:00) sent my application for PhD in computer science to the National University of Singapore

[Michael Rothgang]

Good luck!

[Jeremy Tan]

https://github.com/fpvandoorn/carleson/pull/188 <- Lemma 7.4.1

[Floris van Doorn]

Welcome back, Jeremy. Exciting to hear that you've applied for PhD positions! I wish you the best of luck with your PhD application.

[Joris Roos]

Lemma 7.4.2 and other things -> https://github.com/fpvandoorn/carleson/pull/192

[Evgenia Karunus]

Just finished 86. Prove Lemma 7.5.1 (PR).
I'd like to take 95. Prove Lemma 7.5.10 next!

[Sébastien Gouëzel]

Can I claim 49 (lemma 5.1.2)?

[Floris van Doorn]

I added your claims to the list.

[James Sundstrom]

Claiming 68 (Lemma 7.1.3).

PR

[Sébastien Gouëzel]

PR for Lemma 5.1.2 at https://github.com/fpvandoorn/carleson/pull/199 (+1282/−127). Tell me if it's too long and you want me to split it.

[James Sundstrom]

I'll claim 69 (Lemma 7.1.4).

Inequality (1.0.7) from the blueprint bounds a certain supremum. But the version in Lean (CompatibleFunctions.localOscillation_le_cdist in Defs.lean) uses the real-valued supremum, which is 0 when the usual supremum would be infinity. So the current version of the inequality actually says that the supremum is either small or infinite. I assume that was not intentional, so I'm planning to change the definition of localOscillation to use ENNReal instead.

On a quick search through the blueprint, it looks like the only other place where inequality (1.0.7) is used is in Lemma 7.5.5, which is the currently-unclaimed task 90, so I don't think this should cause any issues. If anyone wants to claim task 90 before I'm done with task 69, we should probably talk.

EDIT: PR

[Sébastien Gouëzel]

I'd like to claim 110 (Lemma 5.1.3).

[Floris van Doorn]

Seems like there was great progress while I was having holidays :tada:
@James Sundstrom Yes, changing the supremum to ENNReal is good. This was a remnant from the starting design decisions, where I tried to do everything in ℝ, before realizing how much of a pain that was.
I'll take a look at the opened PRs now.

[Sébastien Gouëzel]

PR for Lemma 5.1.3 at https://github.com/fpvandoorn/carleson/pull/200.

[Sébastien Gouëzel]

I've started upstreaming some auxiliary results of my argument, in #20419.

[Evgenia Karunus]

I'd like to take on 88. Prove Lemma 7.5.3!

[Pietro Monticone]

Sébastien Gouëzel said:

I've started upstreaming some auxiliary results of my argument, in #20419.

You might want to report upstreaming updates here: https://leanprover.zulipchat.com/#narrow/stream/442935-Carleson/topic/Upstream.20to.20Mathlib

[Sébastien Gouëzel]

It's about things that have not yet been merged by Floris, so what should be done here is not clear to me. By the way, I'm preparing a mathlib bump currently to latest mathlib, to make sure that we can use everything that has already been upstreamed. Going smoothly so far...

[Sébastien Gouëzel]

Bump PR at https://github.com/fpvandoorn/carleson/pull/202. Depending on whether #20456 and #20457 (which are upstreaming PRs) get in Mathlib quickly, it might make sense to update it before merging it.

[Pietro Monticone]

@Sébastien Gouëzel I have just added two steps in the push_pr.yml workflow file to test the bump of carleson in the docbuild project (see here for the commit diff).

Would you mind if I merge master into Carleson#202 to update your PR branch? This will allow us to conduct a final test of what I claimed here and ensure everything works as expected for future bump PRs as well.

[James Sundstrom]

I'll claim Task 71 (Lemma 7.1.6)

Edit: PR

[Sébastien Gouëzel]

Pietro Monticone said:

Would you mind if I merge master into Carleson#202 to update your PR branch? This will allow us to conduct a final test of what I claimed here and ensure everything works as expected for future bump PRs as well.

Sure, go ahead!

[Pietro Monticone]

Done and it worked as expected :check:

[Floris van Doorn]

Thanks for the new PRs! I merged the bump PR first, so if you have another open PR or are working on one, please merge master!

[James Sundstrom]

I'll take Task 72 (Lemma 7.2.1)

Edit: PR. If anyone wants to claim Tasks 73 or 74 (Lemma 7.2.2 or Lemma 7.2.3), note that I changed the statements slightly.

[Joris Roos]

Lemma 7.6.1 and a bit more in BoundedCompactSupport in this PR

[James Sundstrom]

Claiming Task 73 (Lemma 7.2.2)

PR

[Evgenia Karunus]

I'd like to take on 96. Prove Lemma 7.5.11!