Paper writing tasks

Stream: Carleson

[María Inés de Frutos Fernández]

Hi everyone! It is time to start drafting the Carleson formalization paper.

Each of the tasks below corresponds to drafting a (sub)section of the paper. Keep in mind that these are preliminary sections so that we can split the work, but some of them might be reorganized or combined later on.

Remember that whatever you write in the paper will likely get edited by others.

Tasks:

1 :new: 1.1. Brief history of Carleson’s theorem and significance
2 :play:(@María Inés de Frutos Fernández) 1.2. Overview of the formalization project
3 :new: 1.3. Related work
4 :play: (@Leo Diedering) 2.1. Mathematical background
5 :play: (@Jasper Mulder-Sohn) 2.2. Statement of the main results
6 :play: (@Floris van Doorn) 3. Project organization
7 :new: 4.1. The blueprint writing process
8 :new: 4.2. Changes and refinements
9 :new: 4.3. Dealing with mistakes
10 :new: 4.4. Lessons learned
11 :play: (@María Inés de Frutos Fernández) 5.1. Treatment of constants
12 :play: (@Sébastien Gouëzel) 5.2. The ProofData pattern
13 :play: (@Jim Portegies ) 5.3. Working with real numbers
14 :play: (@Michael Rothgang) 5.4. Use of ENorm
15 :new: 5.5. Working with Lp functions
16 :play: (@Joris Roos) 5.6. The BoundedCompactSupport structure
17 :new: 5.7. Common pitfalls
18 :new: 6. Conclusion

[Floris van Doorn]

Thanks for posting this, Maria! @channel For the authors of the formalization: please contribute a subsection!

[Sébastien Gouëzel]

Can I take 12?

[Jim Portegies]

I could give 13 a try, if I understand what is meant there. I had my own experiences with the real numbers, but i also remember talks by Floris where he mentioned for instance suprema first taking values in the real numbers, but later switched to extended real numbers because it was quite inconvenient.

[Joris Roos]

I volunteer for 16

[María Inés de Frutos Fernández]

Thank you to everyone who volunteered! I updated the list.

[Leo Diedering]

I can try to draft some parts of 4 (Mathematical background).
Maybe later I could also add something to 13 or 14 when @Jim Portegies resp. @Michael Rothgang are finished since I also had some experience with both of these topics (I think the switch to ENNReal was partly in response to my problems with suprema over the real numbers).

[Jasper Mulder-Sohn]

When I have a look at the sections still available, I think I could contribute the most to chapter 3 (if split to subsections is an option there). I'm also happy to review and add to other subsections when a first draft is available.
If chapter 3 is not available, I could try task 5 but I don't feel 100% confident about that.

[María Inés de Frutos Fernández]

Chapter 3 is taken by Floris, do you want to give task 5 a go? The blueprint should provide a good starting point for that.

[Jasper Mulder-Sohn]

Alright, I'll give task 5 a shot :thumbs_up: