Finalizing Tasks

Stream: Carleson

[Floris van Doorn]

The formalization is essentially finished, except for cleaning up/finishing PR fpvandoorn/carleson#449.

There is some tasks to clean up the formalization and improve the presentation.

1. It would be nice if Carleson.Defs contains the statements MetricSpaceCarleson : Prop, LinearizedMetricCarleson : Prop and ClassicalCarleson : Prop of metric_space_carleson, linearized_metric_carleson and classical_carleson and only the definitions used in these statements (including DoublingMeasure). Everything else should go in separate files (preferably split by topic, but Carleson.FurtherDefs + Carleson.Lemmas is also acceptable). I want to make it as easy as possible to check that the statements of those theorems match the blueprint's.
2. Move the class DoublingMeasure out of ToMathlib (the definition to Defs, the rest elsewhere). The class IsDoubling should stay in ToMathlib.
3. Double check that these definitions/statements are as closely aligned as the blueprint as reasonably possible (preferably by changing the formalization when there is a mismatch, except if it's in the constants). fpvandoorn/carleson#454 fixes two mismatches.
4. Check that the statements of chapter 2 align with the formalized statements. Double check whether the constants were updated in the formalization, but these changes are not yet incorporated in the blueprint.
5. There are a few proofs that were done differently in the formalization and the blueprint. Notably, we prove the Marcinkiewicz interpolation theorem for chapter 9. @Jim, maybe you can add the statement of this into chapter 9? For the proof, I think it's fine to refer to a standard source (or a standard source pointing out a few differences). A fully written proof is of course also welcome, but not necessary.
6. Other cleanups in the Lean files are also welcome! E.g. removing outdated comments/todos/commented out code, or refactoring proofs. If you move code between files, try change as little as possible in that commit, for ease of reviewing.
7. Checking that the lemmas in the rest of the blueprint align with the Lean formalization is also useful, but not super important (in some cases there is a bit of freedom taken in the translation, which is fine). If someone wants to check that the constants match the formalization's constants, that might be good.

Help is very welcome! Feel free to claim one of these tasks (or a part of it).

[Michael Rothgang]

@Jim Portegies on the above (I believe Floris wanted to @ mention you)

[Jasper Mulder-Sohn]

Ad 4.:

• I have verified Proposition 2.0.1 to be identically formalized, except the constants for 2.0.1 and 2.0.2 (they are equal) are formally defined as the sum of the two smaller constants 5.1.2 and 5.1.3 link. Also the definition of carlesonOn does not use the definition of Ks but instead its unfolded equivalent. I guess this could be fixed.
• I have verified Propositions 2.0.3, 2.0.4 to be identically formalized including constants
• For Proposition 2.0.5 the assumption on the finiteness of the Holder norm for $\psi$ is not included in the formalization, I guess the formalized statement also holds for the infinite case. The Holder norm definition (link) includes the ProofData assumption which should not be needed.
• For Proposition 2.0.6 I notice that we assume that $\mu$ is doubling, is that intended? I wasn't able to verify the value of the constant C2_0_6 link due to underlying complexity.
• For the statement about the global maximal function, the formalization assumes $0 < p_1$ and the blueprint $1 \le p_1$.

NB. In the above, I have taken the liberty to assume that all the (deeper) notation used in the blueprint is acceptably formalized because I am not familiar with all the constructions. Depending on the strictness desired, this could still be done.

Is it intended that also section 2.1 is checked?

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

Floris van Doorn said:

Other cleanups in the Lean files are also welcome! E.g. removing outdated comments/todos/commented out code, or refactoring proofs. If you move code between files, try change as little as possible in that commit, for ease of reviewing.

I will do this for the files in the Antichain folder.

[Jeremy Tan]

fpvandoorn/carleson#464: I replace most of the nnnorm uses with enorm (proofs must be rewritten for this). In about 12 hours' time though, I'll be taking off to hike Mount Fuji

[Jeremy Tan]

2025-07-19T00:55:00+08:00

[Jasper Mulder-Sohn]

Jasper Mulder-Sohn said:

Ad 4.:

• I have verified Proposition 2.0.1 to be identically formalized, except the constants for 2.0.1 and 2.0.2 (they are equal) are formally defined as the sum of the two smaller constants 5.1.2 and 5.1.3 link. Also the definition of carlesonOn does not use the definition of Ks but instead its unfolded equivalent. I guess this could be fixed.
• I have verified Propositions 2.0.3, 2.0.4 to be identically formalized including constants
• For Proposition 2.0.5 the assumption on the finiteness of the Holder norm for $\psi$ is not included in the formalization, I guess the formalized statement also holds for the infinite case. The Holder norm definition (link) includes the ProofData assumption which should not be needed.
• For Proposition 2.0.6 I notice that we assume that $\mu$ is doubling, is that intended? I wasn't able to verify the value of the constant C2_0_6 link due to underlying complexity.
• For the statement about the global maximal function, the formalization assumes $0 < p_1$ and the blueprint $1 \le p_1$.

NB. In the above, I have taken the liberty to assume that all the (deeper) notation used in the blueprint is acceptably formalized because I am not familiar with all the constructions. Depending on the strictness desired, this could still be done.

Is it intended that also section 2.1 is checked?

Additionally the statements of section 2.1 were verified, with just one difference: the constant D2_1_3 (link) was replaced to 2 ^ 127 (for c = 100) instead of original 2 ^ 150 in PR fpvandoorn/carleson#458.

This leaves the following (possible) changes as part of this task:

1. Adjust C2_0_2 and make the current definition an inequality lemma
2. Adjust definition of carlesonOn to use Ks
3. Adjust / clean up Holder norm definition (is this a Mathlib upstreaming task?)
4. Proposition 2.0.6 uses a different formalization as I read; what is the intention here? Including assumption mismatch
5. Fix the D2_1_3 constant in the blueprint. This sounds arduous because kernel_summand is at the top of the dependency graph. Maybe this is better suited as a separate follow up task from fpvandoorn/carleson#458?

I can certainly do 1 and 2, but for 3,4,5 some advice would be helpful.

[Sébastien Gouëzel]

I am currently fixing all the constants to let them match the blueprint.

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

Floris van Doorn said:

1. It would be nice if Carleson.Defs contains the statements MetricSpaceCarleson : Prop, LinearizedMetricCarleson : Prop and ClassicalCarleson : Prop of metric_space_carleson, linearized_metric_carleson and classical_carleson and only the definitions used in these statements (including DoublingMeasure). Everything else should go in separate files (preferably split by topic, but Carleson.FurtherDefs + Carleson.Lemmas is also acceptable). I want to make it as easy as possible to check that the statements of those theorems match the blueprint's.
2. Move the class DoublingMeasure out of ToMathlib (the definition to Defs, the rest elsewhere). The class IsDoubling should stay in ToMathlib.

I will work on these two tasks.

[Jasper Mulder-Sohn]

I found myself starting to need this to avoid duplicate work and keep track of progress. Floris, please feel free to take over this post.

Cleanup task overview

1. :check: (Maria) It would be nice if Carleson.Defs contains the statements MetricSpaceCarleson : Prop, LinearizedMetricCarleson : Prop and ClassicalCarleson : Prop of metric_space_carleson, linearized_metric_carleson and classical_carleson and only the definitions used in these statements (including DoublingMeasure). Everything else should go in separate files (preferably split by topic, but Carleson.FurtherDefs + Carleson.Lemmas is also acceptable). I want to make it as easy as possible to check that the statements of those theorems match the blueprint's.
2. :check: (Maria) Move the class DoublingMeasure out of ToMathlib (the definition to Defs, the rest elsewhere). The class IsDoubling should stay in ToMathlib.
3. :new: Double check that these definitions/statements are as closely aligned as the blueprint as reasonably possible (preferably by changing the formalization when there is a mismatch, except if it's in the constants). fpvandoorn/carleson#454 fixes two mismatches.

4. :check: (Jasper) 1. Check that the statements of chapter 2 align with the formalized statements.
   Note: identified issues listed as separate tasks
   :check: (Sebastien) 2. Double check whether the constants were updated in the formalization, but these changes are not yet incorporated in the blueprint.

5. :new: There are a few proofs that were done differently in the formalization and the blueprint. Notably, we prove the Marcinkiewicz interpolation theorem for chapter 9. Jim, maybe you can add the statement of this into chapter 9? For the proof, I think it's fine to refer to a standard source (or a standard source pointing out a few differences). A fully written proof is of course also welcome, but not necessary.

6. :play: Other cleanups in the Lean files are also welcome! E.g. removing outdated comments/todos/commented out code, or refactoring proofs. If you move code between files, try change as little as possible in that commit, for ease of reviewing.
   :check: (Maria) Antichain folder
   :new: Classical folder
   :new: Discrete folder
   :new: ForestOperator folder
   :check: (Jasper) MetricCarleson folder
   :check: (Jasper) TwoSidedCarleson folder
   :check: (Jasper) Main folder

7. :new: 1. Checking that the lemmas in the rest of the blueprint align with the Lean formalization is also useful, but not super important (in some cases there is a bit of freedom taken in the translation, which is fine).
   :check: (Sebastien, fpvandoorn/carleson#473) 2. If someone wants to check that the constants match the formalization's constants, that might be good.

Follow up (sub)tasks
401 :check: The Holder norm definition (link) includes the ProofData assumption which should not be needed
402 :new: Check statement of Proposition 2.0.6 link, particularly constant C2_0_6 and hypothesis $0 < p_1$ (vs blueprint $1 \le p_1$). Is this related to main task 5?
403 :check: Adjust carlesonOn definition to use Ks

[Jeremy Tan]

Jeremy Tan said:

fpvandoorn/carleson#464: I replace most of the nnnorm uses with enorm (proofs must be rewritten for this).

fpvandoorn/carleson#479 does this in the one remaining file

[Michael Rothgang]

Task 4, part (2) was merged

[Jasper Mulder-Sohn]

PR for 403: fpvandoorn/carleson#492

[Jasper Mulder-Sohn]

PR for 401: fpvandoorn/carleson#493 has incorporated the recent bumps, is it possible to wrap this up?

[Floris van Doorn]

Oops, I forgot about that PR. I merged it.