Paper discussion

Stream: Carleson

[Floris van Doorn]

Hi all!

Sorry for the radio silence from my side. I've been working on other things, but I want to return to this project to work on the remaining tasks. This is mostly writing the paper, but also continuing porting results to Mathlib. (see #Carleson > Porting to Mathlib)

[Floris van Doorn]

About the paper-writing process:

1. We want to write a formalization paper about the formalization, describing the organization, the mathematical content (not in detail), the blueprint and design decisions.
2. We want to write this paper collaboratively and in public, which is a bit of a challenge with this many authors.
3. We want to first decide what sections and subsections we want to write, and then we can divide up the different subsections to authors responsible for them.
4. It is not required as an author to write part of the paper. For the authors that might not be entirely comfortable with writing a substantial part of the paper, you can contribute in other ways (editing, proof reading, Mathlib porting)!
5. Just to be clear: even though the writing process is public, making a contribution to the paper does not mean you automatically get added as author. In principle, the author list of the formalization paper is the subset of the blueprint authors that have contributed to the formalization. Non-authors can participate in discussions about the paper.
6. Whatever you write in the paper can/will get edited by others.

[Floris van Doorn]

I would like to discuss the topics we want to write about. As a starting point, @María Inés de Frutos Fernández, @Michael Rothgang and I have already made an outline of the sections we want to see in the paper. The bullet points are things we want to discuss in that section (not necessarily subsections). Everything here is subject to change, so please suggest additions/improvements.

[Floris van Doorn]

Sections

1. Introduction
2. Mathematics
3. Organization
4. Blueprint
5. Design
6. Conclusion

In more detail:

Introduction

• History of the Carleson theorem (summary of blueprint introduction)
• Very brief description of the project
• Related work (other large-scale formalization projects in Lean and other proof assistants, other harmonic analysis formalization)

Mathematics

The mathematics of the project, and how it is formalized. In how much detail do we want to go here?

• prerequisites: Fourier series, Real interpolation,
  Hardy--Littlewood maximal function, doubling measures (IsDoubling), WeakType and wnorm

• statement of Theorem 1.0.2

• the main Propositions in Chapter 2

Organization

Discuss how the project was organized.

• Floris responsible (mostly) for lemma statements (has advantages and disadvantages)
• interaction with harmonic analysis group (Lars answering questions)
• contributors and tasks
• ToMathlib directory; different contributions standards
• Zulip, GitHub, blueprint (mention: github project in e.g. equational theories or FLT)

Blueprint

Discussion on the blueprint (maybe subsection of Organization?)

• Blueprint-writing process
  • using finitary arguments in the proof
• Blueprint changes:
  • $I\leq J$ vs $I\subset J$
  • real interpolation theorem
  • Hardy--Littlewood maximal function for finite vs. countable balls
  • just one top cube (G. Gonthier's remark)
  • tweaking constants
• Mistakes in the blueprint:
  • Lemma 11.1.6, sublemmas didn't quite match
  • Chapter 6 (Lemma 6.3.3/4): proof broke at s(L)=-S/ lemma mismatch
  • Hölder cancellation (Chapter 8): radius R -> 2R
  • maybe: Lemma 6.2.3: additional hypothesis, change conclusion
• Reflections on how certain decisions when writing the blueprint caused small errors.
• Mention: we did not use definition environments (therefore didn't show up in dep graph)

Design Decisions

Design decisions used in the formalization.

• ENorm
• explict constants C_a_b_c
• ProofData pattern
• work with MemLp, not functions on Lp
• Usage of Real vs. NNReal vs. ENNReal
  • Challenge with ENNReal: tactic support, such as norm_num, finiteness, field_simp, ring (1 + 1 = 2 is fine, 1/2 + 1/2 is not)
• BoundedCompactSupport (packaging existing conditions).
  • Ongoing experiments with fun_prop
• mistakes made: usage of Real; usage of Set.indicator vs Measure.restrict
• Finsets vs. Sets in a Fintype

Conclusion

short. Maybe skip?

• project statistics (e.g. size of ToMathlib and full project)
• Summary of lessons learned
  • It's good to refer to general results/generalize, even already when writing the blueprint

[Floris van Doorn]

Suggestions and comments are welcome! Of course, if you, as a contributor, have additional comments that you think are appropriate for the paper, please also discuss them here!

[Floris van Doorn]

After we have discussed the outline for a bit, I will add a subfolder to the Carleson repository, where we can collaboratively write the paper.

[Pietro Monticone]

Thank you @Floris van Doorn, @Michael Rothgang and @María Inés de Frutos Fernández for starting to outline the paper!

Would you like me to set up the same LaTeX paper compilation workflow that we’re using for the Equational Theories project?

[Floris van Doorn]

Yes, please do! Thanks!

[Pietro Monticone]

Ok, tonight or tomorrow night.

[Pietro Monticone]

Done https://github.com/fpvandoorn/carleson/pull/507.

[Pietro Monticone]

Just a simple template https://florisvandoorn.com/carleson/paper.pdf

[Terence Tao]

By the way, in the Equational Theories Project we set up a contributions matrix for different participants to declare which portions of the project they were comfortable being associated with as a co-author: https://github.com/teorth/equational_theories/blob/main/paper/contributions.md . Perhaps our project was more diverse than yours and so such a matrix might not be as necessary for Carleson, but I thought I would mention it.