Outstanding Tasks, V5

Stream: Carleson

[Floris van Doorn]

After a lot of good progress on chapter 7, here is a new list of tasks. There is still work to do in chapter 7, and I also added all lemmas from Sections 10.1 and 11.3. Much of this material is more elementary and requires less knowledge about the definitions in this proof, so they can be nice to try if you want to join!

There is a CONTRIBUTING file that contains some useful tips.

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.

55 :check: (Michael Rothgang and Sébastien Gouëzel) Prove Lemma 8.0.1 (long)
56 :check: (Michael Rothgang and Sébastien Gouëzel) Prove Proposition 2.0.5 (quite long)
73 :check: (James Sundstrom) Prove Lemma 7.2.2
74 :check: (Jeremy Tan) Prove Lemma 7.2.3
76 :check: (James Sundstrom) Prove Lemma 7.3.1
77 :check: (Jeremy Tan) Prove Lemma 7.3.2
78 :check: (James Sundstrom) Prove Lemma 7.3.3
82 :new: Prove Lemma 7.4.4
83 :new: Prove Lemma 7.4.5
84 :new: Prove Lemma 7.4.6
87 :check: (Jeremy Tan) Prove Lemma 7.5.2
89 :new: Prove Lemma 7.5.4
90 :check: (Jeremy Tan) Prove Lemma 7.5.5
92 :check: (Jeremy Tan) Prove Lemma 7.5.7
94 :check: (Jeremy Tan) Prove Lemma 7.5.9
95 :play: (Evgenia Karunus) Prove Lemma 7.5.10
96 :check: (Evgenia Karunus) Prove Lemma 7.5.11
98 :new: Prove Lemma 7.6.2
99 :check: (Jeremy Tan) Prove Lemma 7.6.3
101 :check: (Edward van de Meent) Prove Lemma 7.7.1
102 :play: (Edward van de Meent) Prove Lemma 7.7.2
103 :new: Prove Lemma 7.7.3
104 :check: (Edward van de Meent) Prove Lemma 7.7.4
105 :new: Prove Proposition 2.0.4
109 :check: (Jim Portegies) (see here) make sure that carleson#hasStrongType_globalMaximalFunction is sorry-free. (depends on 117, 118)

For the next 8 tasks see this thread for more information.

111 :check: (Floris van Doorn) Remove toReal from all statements that someOperator . . |>.toReal have weak/strong type. Use carleson#MeasureTheory.hasWeakType_toReal_iff and variants to fix proofs, (you can leave the assumption in that equivalence sorry'd).
112 :check: (Michael Rothgang) Generalize all Mathlib lemmas about MemLp and similar definitions (see changes of #20122 for all "similar definitions") that hold for ENorm to ENorm.
113 :play: (Michael Rothgang) Upstream https://florisvandoorn.com/carleson/docs/Carleson/ToMathlib/ENorm.html (we might need to discuss if we're happy with these exact classes)
114 :play: (Michael Rothgang) Generalize all Mathlib lemmas that can be generalized to one of the classes in 113 to the appropriate class. (depends on 113)
115 :play: (Michael Rothgang) Generalize all results in WeakType.lean to ENorm-classes (depends partly on 112, 114)
116 :play: (Michael Rothgang) Generalize the proof of the real interpolation theorem to also include operators mapping into ENNReal A start of this has been made in #209 (depends partly on 114, 115)
117 :new: Fix all sorry's introduced in 111 by translating all the proof so that they use ENNReal directly. (depends on 115, 116)
118 :check: (Jim Portegies) Prove carleson#hasStrongType_maximalFunction without the assumption hR that the radii of the balls are bounded above (cf. carleson#hasStrongType_maximalFunction_todo). A proof for basically this result is given in Chapter 9, everything following after equation (9.0.36). EDIT: We also included carleson#hasWeakType_maximalFunction in this.

119 :check: (Bolton Bailey) Prove Lemma 10.1.1
120 :check: (Jasper Mulder) Prove Lemma 10.1.2
121 :check: (Leo Diedering) Prove Lemma 10.1.3
122 :play: (Jasper Mulder) Prove Lemma 10.1.4
123 :play: (Jasper Mulder) Prove Lemma 10.1.5
124 :play: (Jasper Mulder) Prove Lemma 10.1.6
125 :new: Prove Lemma 10.1.7
126 :new: Prove Lemma 10.1.8
127 :new: Prove Lemma 10.0.2

128 :new: Prove Lemma 11.3.1
129 :check: (James Sundstrom) Prove Lemma 11.3.3 This is a special case of Young's convolution inequality. Bonus points if you formalize a general version first!
130 :new: Prove Lemma 11.3.4
131 :new: Prove Lemma 11.3.5
132 :new: Prove Lemma 11.1.6 (hard)
133 :check: (Leo Diedering) Prove Lemma 11.1.11: this is already mostly formalized from Mathlib-results, but with a different formulation (see Lean file)

134 :check: (Clara Torres) Prove carleson#MeasureTheory.HasWeakType.const_smul (and add similar lemmas for MemWℒp, wnorm, etc. that are needed for the proof). Easy
135 :play: (Jim Portegies) Prove that the Hardy-Littlewood maximal function is lower-semicontinuous: carleson#continuous_average_ball, carleson#lowerSemiContinuous_MB and carleson#lowerSemiContinuous_globalMaximalFunction. This is not proven in the blueprint, but you can refer to e.g. [Folland, Real Analysis. Modern Techniques and Their Applications, Section 3.4]
136 :new: Prove Lemma 10.2.2
137 :new: Prove Lemma 10.2.4
138 :new: (Clara Torres) Prove Lemma 10.2.5. This lemma has a long statement and proof. I already formalized a skeleton of the proof, and this now consists of 21 sorry'd statements in the section "Lemma 10.2.5", most of which are pretty easy. Feel free to claim only part of these sorry's.
139 :new: Prove Lemma 10.2.6
140 :new: Prove Lemma 10.2.7 (long)
141 :new: Prove Lemma 10.2.8
142 :new: Prove Lemma 10.2.9
143 :new: Prove Lemma 10.0.3
144 :new: Prove Theorem 10.0.1

---

After this, the only things that still need to be done are in Section 3 (and maybe a few sorry's I missed).
Section 3 is being rewritten to also contain the proof of another general theorem, Theorem 1.0.3.

[Yaël Dillies]

FYI I need Young's convolution inequality for APAP too, so extra bonus points for a general version!

[Bolton Bailey]

I'd like to try 10.1.1 if that's all right.

[James Sundstrom]

I'll try Young's convolution inequality (Task 129, Lemma 11.3.3)

[Edward van de Meent]

i'm giving forest row decomposition a go (Task 101, Lemma/def 7.7.1)

[Michael Rothgang]

I'm also working on tasks 113 and 114 (and hope nobody else started that yet; otherwise, I'm of course happy to share work/discuss).

[James Sundstrom]

@Yaël Dillies Since you were interested, my proof of Young's convolution inequality is here

[Edward van de Meent]

i'm also taking a stab at 7.7.4

[Jeremy Tan]

Lemma 7.2.3: https://github.com/fpvandoorn/carleson/pull/241

[Jeremy Tan]

Most of Lemma 7.5.5 has been pushed to https://github.com/fpvandoorn/carleson/pull/246. Once again I found another mistake, this time involving confusion between open and closed balls; this is described in that PR description

[Floris van Doorn]

I just merged https://github.com/fpvandoorn/carleson/pull/224, stating all lemmas in Section 10.2, and I added tasks 134-144 to prove those lemmas. As far as I can tell, these tasks formalize everything except chapter 3.

[James Sundstrom]

I'll take Lemma 7.3.1 (Task 76)

[Evgenia Karunus]

Lemma 7.5.11 is ready (github.com/fpvandoorn/carleson/pull/238)

[Edward van de Meent]

i'm taking a look at 7.7.2

[Jeremy Tan]

Lemma 7.5.2: https://github.com/fpvandoorn/carleson/pull/249

[Jeremy Tan]

I have put the proof of Lemma 7.6.3 in the same PR above

[James Sundstrom]

I might be missing something, but I don't quite follow how Lemma 7.3.3 is being used in the proof of Lemma 7.3.1. Lemma 7.3.3 has an assumption about the existence of a certain q, and I don't see how we can guarantee that assumption always holds in Lemma 7.3.1. But I also don't think the assumption is necessary to prove Lemma 7.3.3. So I'll claim 7.3.3 also, to try to prove it without the q assumption.

[Floris van Doorn]

Lars said to me that the proof of Lemma 7.3.1 is not correct, and will push a fix to the blueprint later.

[Floris van Doorn]

Message from Lars about 7.3.1 & 7.3.3:

The assumption is indeed used in a fairly stupid way, but it has to be
there: It is used to guarantee that J', which has scale one larger than J,
exists. It only exists if the scale of J is not already maximal. And if J
is some cube in the partition that lives very far away from I(u), then
indeed it will be of scale S and this will go wrong. So one has to assume
that J is somewhat close to some tile from the tree.
I think there is a cleaner way of doing this and fixing the proof of Lemma
7.3.1 at the same time. Our trees are all 'normal', i.e. they satisfy
(2.0.37), which implies that really only f restricted to I(u) contributes
in Lemma 7.3.1. So we only need Lemma 7.3.3 for J contained in I(u), and
in that case it is easy to see that J' exists.
I am changing the blueprint now. The argument why one can replace f by its
restriction to I(u) in Lemma 7.3.1 is essentially contained in the second
statement of Lemma 7.4.1. I am not sure what the best way is to go about
this, but at least whoever formalizes 7.3.1 should probably be aware of
that.

[James Sundstrom]

I already basically finished formalizing the proofs of 7.3.1 and 7.3.3; I'm just cleaning up now. I can edit the blueprint to reflect the way I proved them. (It's true that the proof runs into an issue if J has scale S, but that case is fairly trivial for other reasons.)

[Jeremy Tan]

I've pushed most of Lemma 7.3.2 to https://github.com/fpvandoorn/carleson/pull/254. But I still can't prove one thing, as described at the PR:

Still pending two sorries (L106, L108). If the following was true I could prove them, but it doesn't seem true in general (smul_four_le isn't strong enough):

-- t is a Forest
lemma 𝒬_mem_Ω (hu : u ∈ t) (hp : p ∈ t u) : 𝒬 u ∈ Ω p := by
  sorry

Or am I missing something obvious?

[Jeremy Tan]

Lemma 7.5.9 is at https://github.com/fpvandoorn/carleson/pull/257. I have found two rather serious errors in the blueprint there

[Jim Portegies]

Can I claim Task 118?

[Floris van Doorn]

Yes :smile: Please take a look at #Carleson > Hardy-Littlewood maximal principle for countable many balls to see the ongoing changes to generalize HasWeakType-like declarations to use ENorm. The short version is: just use hasWeakType_toReal_iff sorry freely until we can conveniently do the whole proof for ENormedSpace (or a similar class)

[Michael Rothgang]

To avoid duplicate work: I'm currently bumping Carleson to the latest mathlib.

[Michael Rothgang]

#258 is that bump (it built, CI hasn't fully finished yet)

[Ruben Van de Velde]

https://github.com/fpvandoorn/carleson/pull/258

[Floris van Doorn]

Thanks! I merged it, so the Carleson repo now depends on a new Mathlib.

[Michael Rothgang]

I'd like to also claim 115 (at least for the moment)

[Michael Rothgang]

And I would like to claim task 116

[Sébastien Gouëzel]

Bump PR at https://github.com/fpvandoorn/carleson/pull/293

[Jim Portegies]

I have proved hasStrongType_maximalFunction_todo in the context of Task 118, https://github.com/fpvandoorn/carleson/pull/294

I would be happy with any feedback.

Does Task 118 also encompass hasWeakType_maximalFunction?

[Floris van Doorn]

Great! I'll try to take a look at your PR tomorrow (and the other open PRs).
I forgot that hasWeakType_maximalFunction was another task. I believe it's not hard. If you want to do it as part of task 118, great! (Otherwise I'll create a new task for it.)

[Jim Portegies]

Floris van Doorn said:

Great! I'll try to take a look at your PR tomorrow (and the other open PRs).
I forgot that hasWeakType_maximalFunction was another task. I believe it's not hard. If you want to do it as part of task 118, great! (Otherwise I'll create a new task for it.)

Yes I'd be happy to do it as part of task 118 :)

[Jim Portegies]

I have created a new PR, #315 for task 118. It builds on top my previous PR, #294. Didn't quite know if I should make a new one or push to the old one, but went for this solution in the end.

Please note that I adapted the constant in the weaktype estimate: I do not quite know how to circumvent that. If needed, I could think about it further.

[Floris van Doorn]

Thanks! I merged both your PRs.

[Jasper Mulder-Sohn]

I would claim tasks 122, 123, 124 if that's alright (lemmas 10.1.4, 5, and 6)

[Floris van Doorn]

Cool, sure!

[Floris van Doorn]

There is also still a sorry in Lemma 10.1.2. Are you also planning to finish that one?

[Jasper Mulder-Sohn]

Floris van Doorn said:

There is also still a sorry in Lemma 10.1.2. Are you also planning to finish that one?

Yes that's also on the list. I might start a topic here if I can't figure it out soon.

[Jim Portegies]

Can I claim 135, the lower-semicontinuity of the maximal function?

[Floris van Doorn]

Sure!