Outstanding Tasks, V3

Stream: Carleson

[Floris van Doorn]

It's time for a new list.
I newly added tasks from Chapter 9. Some results might be missing properties from carleson#MeasureTheory.DoublingMeasure (I stated it without using that class, so that it can be ported to Mathlib more easily). Furthermore, we're not exactly following the blueprint here, to get a more general result, and by using the real interpolation theorem in the proof.

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.
L9. :play: (Leo Diedering) Derive the classical Carleson's theorem from the general version. This is done in chapter 11.
L10. :check: (Jim Portegies) Prove the Real interpolation theorem: carleson#MeasureTheory.exists_hasStrongType_real_interpolation.

9 :check: (Jeremy Tan) Define 𝓩 by Zorn's lemma and prove the properties about it (up to and including the finiteness and inhabited instances).
26 :play: (Austin Letson) Prove Lemma 5.2.9
27 :check: (Jeremy Tan) Prove Lemma 5.2.10
47 :check: (Jeremy Tan) Prove Lemma 5.4.7 (previously 5.4.8)

49. :new: Prove Lemma 5.1.2 using the Lemmas in Section 5.4. Probably hard, but there is already a start of the proof. See also task 65: there is a small inconsistency in the proof.
50. :check: (Jeremy Tan) Prove Proposition 2.0.2 using the Lemmas in Section 5.1. Very short in the blueprint (in Section 5.1), but also serves as a sanity-check of statements of the other lemmas.
51. :check: (Jeremy Tan) Prove Lemma 5.5.1
52. :check: (Joachim Breitner) Generalize the construction of 𝔏₀', 𝔏₁ and 𝔏₃ to a subset of an arbitrary partial order. Prove in this generality that this construction leads to pairwise disjoint antichains and that if the subset has no chains of length $n+1$ then the union of the first $n$ sets is the original set. For 𝔏₃ this construction is applied in the order dual. This proves Lemma 5.5.4 and the first sentence of Lemma 5.5.2.
53. :check: (Jeremy Tan) Prove Lemma 5.5.2 (minus the first sentence - i.e. just prove that it has no chains of length $n+1$)
54. :check: (Jeremy Tan) Prove Lemma 5.5.3
55. :play: (Michael Rothgang) Prove Lemma 8.0.1 (long)
56. :play: (Michael Rothgang) Prove Proposition 2.0.5 (quite long)
57. :check: (James Sundstrom) Prove carleson#Set.Countable.measure_biUnion_le_lintegral. Not hard, the outline is already there.
58. :check: (Jeremy Tan) Prove carleson#MeasureTheory.AEStronglyMeasurable.maximalFunction. Should be an application of a few measurability lemmas.
59. :check: (James Sundstrom) Prove that the Hardy-Littlewood function is sublinear: carleson#MeasureTheory.SublinearOn.maximalFunction. Not hard.
60. :check: (James Sundstrom) Prove carleson#HasWeakType.MB_one. Hard.
61. :check: (Jeremy Tan) Prove carleson#hasStrongType_maximalFunction. Short, not hard.
62. :new: Prove carleson#laverage_le_globalMaximalFunction. Not hard.
63. :new: Prove carleson#hasStrongType_globalMaximalFunction. Easy.
64. :play: (Pietro Monticone) Fill in the four sorries (that are not commented out) in the Defs file
65. ️:check: (Floris van Doorn) There is a mismatch between usages of $k < n$ and $k \le n$, and this leads to a mismatch in the proof of Lemma 5.1.2. We need to replace $<$ by $\le$ in the definition of $G_2$ and the statement of forest_stacking, in both the blueprint and the formalization. A start is made on branch fix_forest_stacking.

There are some rendering issues with plastex in chapter 7. In these cases consult the blueprint pdf which should be fine.

66. :check: (Jeremy Tan) Prove Lemma 7.1.1
67. :check: (Jeremy Tan) Prove Lemma 7.1.2
68. :new: Prove Lemma 7.1.3
69. :new: Prove Lemma 7.1.4
70. :play: (Jeremy Tan) Prove Lemma 7.1.5
71. :new: Prove Lemma 7.1.6
72. :new: Prove Lemma 7.2.1
73. :new: Prove Lemma 7.2.2
74. :new: Prove Lemma 7.2.3
75. :check: (Jeremy Tan) Prove Lemma 7.2.4

[Floris van Doorn]

@Bhavik Mehta Any progress on task 9? Shall I unassign you and open up the task for someone else?

[Bhavik Mehta]

Floris van Doorn said:

Bhavik Mehta Any progress on task 9? Shall I unassign you and open up the task for someone else?

Some progress, unpushed. To make this concrete, let's say unassign me if there's no update before Sunday, does that sound reasonable to you?

[Jeremy Tan]

Since Task 9 was unclaimed, here it is: https://github.com/fpvandoorn/carleson/pull/97

[Jeremy Tan]

Lemma 5.2.10 and Task 58: https://github.com/fpvandoorn/carleson/pull/105

[Jeremy Tan]

Lemma 5.5.1 and 5.5.3: https://github.com/fpvandoorn/carleson/pull/106

[James Sundstrom]

Claiming task 59.

[Jeremy Tan]

(Note that Breitner has effectively done Task 52)

[Jeremy Tan]

Regarding Lemma 5.5.1: the blueprint states that the decomposition goes up to 𝔏_3, implying that the forest union 𝔓₁ starts from ℭ_4, but the forest union lemma proof assumes 𝔓₁ starts from ℭ_5. This must be a gap in the blueprint – is 𝔏_4 missing from the antichain decomposition?

[Jeremy Tan]

(i.e. is an 𝔏_4 antichain lemma missing?)

[Jeremy Tan]

@Floris van Doorn

[Jeremy Tan]

Actually, please merge https://github.com/fpvandoorn/carleson/pull/109 first to update mathlib4 – this incorporates the breaking changes to minimal/maximal of #14721 (this was quite tough to adapt to, @Peter Nelson)

[Joachim Breitner]

Thanks for also adapting height. Don’t worry too much about cleaning it up stylistically, though, as the code is already copied to https://github.com/leanprover-community/mathlib4/pull/15524 and I’m refining it there. I’ll peek at your changes so that they are not lost.

[Peter Nelson]

Jeremy Tan said:

Actually, please merge https://github.com/fpvandoorn/carleson/pull/109 first to update mathlib4 – this incorporates the breaking changes to minimal/maximal of #14721 (this was quite tough to adapt to, Peter Nelson)

Can you elaborate on the toughness? As @Joachim Breitner pointed out in a couple of comments, some of the rough edges were from your using Minimal s x where s is a Set, which is abusing defeq.

Note also that you shouldn't need to write Minimal univ x or Minimal (fun _ -> True) x, since IsMin x already exists for this purpose.

But there were one or two places you used an awkwardchange, as a result of a lemma that was actually missing. I've made #15554 to address this.

Please let me know if there were any other things that came up.

[Joachim Breitner]

Thanks for the pointer to IsMin, updated my mathlib4 PR

[Jeremy Tan]

Jeremy Tan said:

Regarding Lemma 5.5.1: the blueprint states that the decomposition goes up to 𝔏_3, implying that the forest union 𝔓₁ starts from ℭ_4, but the forest union lemma proof assumes 𝔓₁ starts from ℭ_5. This must be a gap in the blueprint – is 𝔏_4 missing from the antichain decomposition?

I noticed this potential issue just before updating the Carleson project to the latest mathlib

[Floris van Doorn]

I was on a break for a few days. I'll try to comment on everything today.

[Jeremy Tan]

Another proof gap, this time in Lemma 6.1.2: "This (Equation 6.1.8) together with a ≥ 1 proves the Lemma." But in order to say this the form $B(x,8D^{\mathrm s(\mathfrak p)})$ must be a ball in 𝓑, which cannot be guaranteed to be the case

[Jeremy Tan]

since 𝓑 consists of balls of the form $B(\mathrm c(\mathfrak p),8D^{\mathrm s(\mathfrak p)})$ and x is arbitrary

[James Sundstrom]

I made a PR for Task 60 that's mostly complete, except for a sorry that would be trivial for finite 𝓑, but I don't see how to make it work for countable 𝓑.

[Jim Portegies]

I made a PR for the real interpolation theorem.

[Johan Commelin]

Link to PR: https://github.com/fpvandoorn/carleson/pull/115

Diff size: +4,990 −37

That's an epic!

[Johan Commelin]

Congratulations with finishing this!

[Michael Rothgang]

That is impressive. I look forward to this slowly reaching mathlib!

[Michael Rothgang]

I am happy to tackle items 55 and 56 (but cannot promise this will happen before October)

[Michael Rothgang]

In case another opinion is helpful: I just looked at PRs #112, #113 and #114 on the repo; I think they can all be merged.

[Floris van Doorn]

I'm back from holiday. I'm still at the ITP conference, but I should have time to answer questions and merge PRs again.

Thanks for all the great work many of you have done while I was away. Especially thanks to Jim for the real interpolation theorem!

[Floris van Doorn]

James Sundstrom said:

I made a PR for Task 60 that's mostly complete, except for a sorry that would be trivial for finite 𝓑, but I don't see how to make it work for countable 𝓑.

Thanks! I filled in the first sorry by refining the Vitali-argument a little bit for balls, and the second sorry was (I think) just a missing assumption on the theorem.

[Floris van Doorn]

Michael Rothgang said:

I am happy to tackle items 55 and 56 (but cannot promise this will happen before October)

Ok, great! Thanks!

[Floris van Doorn]

Jeremy Tan said:

Another proof gap, this time in Lemma 6.1.2: "This (Equation 6.1.8) together with a ≥ 1 proves the Lemma." But in order to say this the form $B(x,8D^{\mathrm s(\mathfrak p)})$ must be a ball in 𝓑, which cannot be guaranteed to be the case

Please don't work on this, since Maria is working on this exact proof as well. I will post some more tasks from later parts of chapter 6 and from chapter 7 that you can claim.
Are the remaining open tasks too complicated mathematically? I believe task 53 is not too hard and unclaimed?

[Floris van Doorn]

I updated the first post, but I might have forgot to update some statuses. Please let me know if something is not listed correctly.

[Floris van Doorn]

I stated the lemmas in section 7.1 and (almost) in section 7.2. Feel free to claim these as well!
Some things to note

• Some of these proofs are hard. The first two lemmas in section 7.1 shouldn't be too hard though.
• There are some rendering issues with plastex. In these cases consult the blueprint pdf which should be fine.

[Jeremy Tan]

Lemma 5.5.1 for real: https://github.com/fpvandoorn/carleson/pull/122

[Jeremy Tan]

I've seen nothing from @Austin Letson for the last month or so, let alone regarding Task 26. Can I claim it?

[Austin Letson]

Jeremy Tan said:

I've seen nothing from Austin Letson for the last month or so, let alone regarding Task 26. Can I claim it?

Hi! The lean NYC group is still working on it. We are making slow but steady progress and are close to finishing.

[Jeremy Tan]

Wait, what is the Lean NYC group? Which unis is it associated with? Fordham?

[Austin Letson]

It is a few members who live in NYC and meet up via the NYC #Geographic locality to work on Lean projects. I don't think anyone is at a university right now.

[Jeremy Tan]

Floris van Doorn said:
I believe task 53 is not too hard and unclaimed?

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

[Jeremy Tan]

I have done 7.1.1 and 7.1.2. I have also found a critical error in the proof of 7.1.5.
https://github.com/fpvandoorn/carleson/pull/130

[Jeremy Tan]

The upperRadius function is also problematic. If $Q(x)=\theta$, the set in the definition of $R_Q(\theta,x)$ will be the universal set, and by mathlib's definition of sSup the result will be zero, not some top element as would be expected

[Floris van Doorn]

@Jeremy Tan Thanks! I don't have time at the moment to look at your problem in the proof of 7.1.5, but I'll take a look next week.

[Jeremy Tan]

Proposition 2.0.2 proved: https://github.com/fpvandoorn/carleson/pull/131

[Jeremy Tan]

Specifically I can't prove Measurable fun (p : X × X) ↦ (Q p.1) p.2

[Jeremy Tan]

Never mind, I've proved measurability

[Floris van Doorn]

Thanks for proving 2.0.2 and 7.2.4, Jeremy!

[Jeremy Tan]

@Floris van Doorn when I run lake update -Kenv=dev, some imports disappear and I always have to add them back in. Is there a way I can avoid this?

[Pietro Monticone]

Yes, see here.

[Floris van Doorn]

Does lake -R -Kenv=dev update by itself also work?

[Floris van Doorn]

Jeremy Tan said:

I have done 7.1.1 and 7.1.2. I have also found a critical error in the proof of 7.1.5.
https://github.com/fpvandoorn/carleson/pull/130

There was indeed a mistake in the definition (7.1.3), a $<$ should have been a $\le$. This is now fixed in the blueprint and the Lean definition.

[Pietro Monticone]

Floris van Doorn said:

Does lake -R -Kenv=dev update by itself also work?

Yes, it does. Maybe we should change the update_mathlib.sh as follows:

# Update mathlib and the lean toolchain.
curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake -R -Kenv=dev update # The `-R -Kenv=dev` is making sure we also update doc-gen and other dependencies
lake exe cache get

[Floris van Doorn]

done