Outstanding Tasks, V2

Stream: Carleson

[Floris van Doorn]

I prepared some new tasks!
The new tasks are all from Chapter 5 and almost all in DiscreteCarleson.lean. You can quickly skim the proof to see how hard it is. If you don't see an integral, big sum or dens, the proof probably only requires elementary methods (set theory, metric spaces, measures), though it's not necessarily easy.

There is a CONTRIBUTING file that contains some useful tips.

Ongoing tasks:

4 :check: (James Sundstrom) Lemma 2.1.3: three Lean lemmas computing bounds on a binary function. It might be useful to also fill some other sorry's in the file Psi.lean.
9 :play: (Bhavik Mehta) Define 𝓩 by Zorn's lemma and prove the properties about it (up to and including the finiteness and inhabited instances). The finiteness comes from a variant of Θ.finite_of_le_dist.

L3. :check: (Edward van de Meent) Prove Lemma 4.0.1, the proof is in Section 4.1
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 10 11.
L10. :play: (Jim Portegies) Prove the Real interpolation theorem: carleson#MeasureTheory.exists_hasStrongType_real_interpolation. This is an important theorem that is not explicitly mentioned in the blueprint, but will be used a few times. The proof can be found in
Folland, Real Analysis. Modern Techniques and Their Applications, section 6.4, theorem 6.28. It requires quite a lot of analysis and has a 3-page proof.
L11. :check: (Leo Diedering) Generalize the Cotlar inequality and Calderon-Zygmund-decomposition to metric spaces

Unclaimed tasks from V1:

6 :check: (James Sundstrom) Lemma 4.0.3: this requires manipulating some integrals, and also require stating/proving that a bunch more things are integrable.
7 :check: (James Sundstrom) Proposition 2.0.1: the proof is located above and below Lemma 4.0.3. It is not long, but requires quite some manipulation with integrals.
17 :check: (James Sundstrom) Proof the lemmas about carleson#MeasureTheory.wnorm and carleson#MeasureTheory.MemWℒp (optional: develop more API, following docs#MeasureTheory.snorm and docs#MeasureTheory.Lp and similar notions).

New tasks:

18. :check: (James Sundstrom) Prove Lemma 5.2.1 (probably tricky, feel free to reformulate Proposition 2.0.6 if convenient)
19. :check: (Jeremy Tan) Prove Lemma 5.2.2
20. :check: (Jeremy Tan) Prove Lemma 5.2.3
21. :check: (Jeremy Tan) Prove Lemma 5.2.4
22. :check: (Jeremy Tan) Prove Lemma 5.2.5
23. :check: (Jeremy Tan) Prove Lemma 5.2.6
24. :check: (Jeremy Tan) Prove Lemma 5.2.7
25. :check: (James Sundstrom) Prove Lemma 5.2.8
26. :play: (Austin Letson) Prove Lemma 5.2.9
27. :new: Prove Lemma 5.2.10
28. :check: (Austin Letson) Prove Lemma 5.1.1 (very easy)
29. :check: (Jeremy Tan) Prove Lemma 5.3.1
30. :check: (Jeremy Tan) Prove Lemma 5.3.2
31. :check: (Jeremy Tan) Prove Lemma 5.3.3
32. :check: (Jeremy Tan) Prove Lemma 5.3.4
33. :check: (Jeremy Tan) Prove Lemma 5.3.5
34. :check: (Jeremy Tan) Prove Lemma 5.3.6
35. :check: (Jeremy Tan) Prove Lemma 5.3.7
36. :check: (Jeremy Tan) Prove Lemma 5.3.8
37. :check: (Jeremy Tan) Prove Lemma 5.3.9
38. :check: (Jeremy Tan) Prove Lemma 5.3.10
39. :check: (Jeremy Tan) Prove Lemma 5.3.11
40. :check: (Jeremy Tan) Prove Lemma 5.3.12
41. :check: (Jeremy Tan) Prove Lemma 5.4.1
42. :check: (Jeremy Tan) Prove Lemma 5.4.2
43. :check: (Jeremy Tan) Prove Lemma 5.4.3
44. :check: (Jeremy Tan) Prove Lemma 5.4.5
45. :check: (Jeremy Tan) Prove Lemma 5.4.6
46. :check: (Jeremy Tan) Prove Lemma 5.4.7
47. :play: (Jeremy Tan) Prove Lemma 5.4.8
48. :check: (Jeremy Tan) Prove Lemma 5.4.9
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.
50. :new: 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. :new:Prove Lemma 5.5.1
52. :play: (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. :new:Prove Lemma 5.5.2 (minus the first sentence - i.e. just prove that it has no chains of length $n+1$)
54. :new:Prove Lemma 5.5.3
55. :new:Prove Lemma 8.0.1 (long)
56. :new:Prove Proposition 2.0.5 (quite long)

[Floris van Doorn]

Note: there are likely some small mistakes in the constant bounds, and maybe other typos. Please adapt these as needed.

[Jeremy Tan]

Claiming Lemmas 5.2.3, 5.2.4 and 5.3.4 with https://github.com/fpvandoorn/carleson/pull/56

[Jeremy Tan]

The next PR from me does 5.2.2 (https://github.com/fpvandoorn/carleson/pull/59)

[Austin Letson]

Claiming Lemma 5.1.1

[James Sundstrom]

Claiming Proposition 2.0.1

[Jeremy Tan]

5.2.5 and 5.2.6 are done https://github.com/fpvandoorn/carleson/pull/66

[Floris van Doorn]

James Sundstrom said:

Claiming Proposition 2.0.1

Very good! It's very possible some integrability results are missing. Please add the integrability lemmas you need, and feel free to leave them sorried on the first pass. I hope everything is stated correctly in Lean :-)

[Floris van Doorn]

Oh, you already finished it. Great :-) I wasn't sure how much work these "final steps" would be.

[James Sundstrom]

I'll claim integrable_tile_sum_operator(preliminary to Lemma 4.0.3). If someone else wants to claim the main lemma, that's fine with me though.

[James Sundstrom]

I guess I'll claim Lemma 4.0.3 then.

[Jeremy Tan]

5.3.5 to 5.3.12 are done https://github.com/fpvandoorn/carleson/pull/71

[Floris van Doorn]

Jeremy Tan said:

5.3.5 to 5.3.12 are done https://github.com/fpvandoorn/carleson/pull/71

That's amazing! Unfortunately there was a typo in the definition of dens1, which made Lemma 5.3.11 much easier. Sorry about that. But amazing that you did 7 other lemmas!

[Floris van Doorn]

And you gave the new proof very quickly. Thanks!

[Floris van Doorn]

Since Jeremy is so quick, I also added the lemmas from Section 5.4 as tasks.

[Jeremy Tan]

There's a mistake with the primes in the proof of the symmetry part of Lemma 5.4.2. It should be "If $\mathfrak u \ne \mathfrak u'$, then there exists $\mathfrak p \in \mathfrak{T}_1(\mathfrak u)$ with $10\mathfrak p\lesssim \mathfrak u'$` – no prime after the third $\mathfrak u$, prime after the fourth one

[Jeremy Tan]

I don't know how to fix the proof after correcting for this. I know $2\mathfrak p\lesssim\mathfrak u$ and $10\mathfrak p\lesssim\mathfrak u'$ but need to conclude $2\mathfrak p\lesssim\mathfrak u'$

[Yaël Dillies]

Surely that follows from the former?

[Jeremy Tan]

Yaël Dillies said:

Surely that follows from the former?

$\lesssim$ is defined such that $10\mathfrak p\lesssim2\mathfrak p$ is true and $2\mathfrak p\lesssim10\mathfrak p$ is false

[Jeremy Tan]

lemma smul_mono_left {l l' : ℝ} {p : 𝔓 X} (h : l ≤ l') : smul l' p ≤ smul l p := by
  simp [TileLike.le_def, h, ball_subset_ball]

[Floris van Doorn]

Jeremy Tan said:

I don't know how to fix the proof after correcting for this. I know $2\mathfrak p\lesssim\mathfrak u$ and $10\mathfrak p\lesssim\mathfrak u'$ but need to conclude $2\mathfrak p\lesssim\mathfrak u'$

I might not get to it today, but I'll take a look at that proof.

[Sébastien Gouëzel]

Without having looked at the code at all (but I'm planning to help in a few weeks if you're not done yet), may I complain that this looks like a very bad definition for \le?

[Floris van Doorn]

The order is indeed confusing: it's an order on a product, where in the second component we take the order dual...

[Jeremy Tan]

Floris van Doorn said:

Jeremy Tan said:

5.3.5 to 5.3.12 are done https://github.com/fpvandoorn/carleson/pull/71

That's amazing! Unfortunately there was a typo in the definition of dens1, which made Lemma 5.3.11 much easier. Sorry about that. But amazing that you did 7 other lemmas!

Hold your enthusiasm – all those lemmas were very closely related, down to the proofs, which themselves were quite short. Indeed I reused one proof almost verbatim for another, as I noted in the blueprint

[Floris van Doorn]

Still, you're putting a lot of effort in this project, and I appreciate it!

[Jeremy Tan]

Anyway it's Saturday and academics are more interested right now in whether Krejčíková or Paolini will win at Wimbledon

[Jeremy Tan]

:flag_czechia:

[James Sundstrom]

Claiming Lemma 5.2.1

[Austin Letson]

5.1.1 is done with a big thanks to @Julian Berman for collaborating on the proof!

[Floris van Doorn]

Great! Thanks.
Do you want to also take a look at Lemma 5.2.9 at some point, or shall I remove your name from that one?

[Austin Letson]

We can leave it assigned to me for now. I want to take a look. Thanks Floris!

[Floris van Doorn]

Jeremy Tan said:

There's a mistake with the primes in the proof of the symmetry part of Lemma 5.4.2. It should be "If $\mathfrak u \ne \mathfrak u'$, then there exists $\mathfrak p \in \mathfrak{T}_1(\mathfrak u)$ with $10\mathfrak p\lesssim \mathfrak u'$` – no prime after the third $\mathfrak u$, prime after the fourth one

You're right, the proof as currently written doesn't work. I'm currently discussing a fix with my coauthors.

[Floris van Doorn]

The $\mathfrak{p}$ in the proof should be chosen as an arbitrary element $\mathfrak{p} \in \mathfrak{T}_1(u')$ obtained by $\mathfrak{u'} \in \mathfrak{U}_2(k, n, j)$, and not by using $\mathfrak{u}\sim \mathfrak{u'}$. The rest of the proof should work as written. I pushed a fix (written by Lars) just now.

[Jeremy Tan]

I will be claiming 5.2.7 now – this is unexpectedly very tough due to requiring an invocation of the layercake representation

[Jeremy Tan]

I have had draft code for that for a few days now

[Jeremy Tan]

Floris van Doorn said:

The $\mathfrak{p}$ in the proof should be chosen as an arbitrary element $\mathfrak{p} \in \mathfrak{T}_1(u')$ obtained by $\mathfrak{u'} \in \mathfrak{U}_2(k, n, j)$, and not by using $\mathfrak{u}\sim \mathfrak{u'}$. The rest of the proof should work as written. I pushed a fix (written by Lars) just now.

It (Lemma 5.4.2) is done now

[Jeremy Tan]

5.4.5 to 5.4.7: https://github.com/fpvandoorn/carleson/pull/79

[James Sundstrom]

Claiming Lemma 5.2.8

[Edward van de Meent]

i've all of 4.1 complete, now working on 4.0.1... and i've discovered that we'd like o to be in $Y_k$ when $k = S$, and that doesn't seem to be something that is always the case, right? or is there something i'm missing?

[Edward van de Meent]

for now i'll try and see if i can adapt the definition to require o to be in $Y_S$, but i'm not quite certain everything will work out yet? i'll have to see...

[Floris van Doorn]

Yes, I think you want to choose a maximal set $Y_k$ such that o is in $Y_k$ (I don't think you need that $Y_k$ has maximal cardinality, just that it is maximal w.r.t. set-inclusion, so this is no problem).

[Edward van de Meent]

the variation you suggest i already implemented, but it's good to know it wasn't a bad idea. For now i'm only requiring it when k=S, see how that goes...

[Edward van de Meent]

it turns out the definition of grid structure uses a slightly annoying/(wrong?) version of 2.0.11. in the proof of 4.1.6 we need the assumption that $X \setminus I_3(y,k)$ is nonempty, while we cannot assume this if we use the notation using the real-valued infDist, due to it defaulting to 0 rather than infinity for empty sets

[Edward van de Meent]

one fix is switching the definition to using infEDist, another is switching to specifying that the relevant set is nonempty, rather than messing about with infDist

[Floris van Doorn]

Ah, that might be an error translating from the blueprint to Lean.
I think we allow for the case that cubes can be all of X, so please switch to infEDist.

[Floris van Doorn]

(and quantify over t : ℝ≥0)

[Jeremy Tan]

oh yeah, I forgot to mention: https://github.com/fpvandoorn/carleson/pull/81 is 5.2.7

[Edward van de Meent]

i've run into another issue in 4.0.1. For property 2.0.11, the blueprint says to use lemma 4.1.9. this only covers the case where $t < 1$, and it's not clear (to me) that in the remaining case (with $1 \leq t$) the statement is true?

[Jeremy Tan]

There seems to be a slight snicko in the proof of 5.4.9 though. "By (2.0.8), either $\mathcal I(\mathfrak u) \subset \mathcal I(\mathfrak u')$ or $\mathcal I(\mathfrak u') \subset \mathcal I(\mathfrak u)$", where $\mathfrak{u,u'}\in\mathfrak U_3$ – I don't see how this (non-disjointness of $\mathcal I(\mathfrak u')$, $\mathcal I(\mathfrak u)$) follows from $100\mathfrak u\lesssim m$ and $100\mathfrak u'\lesssim m$

[Jeremy Tan]

If it were the other way around $m\lesssim 100\mathfrak u$ I'd be able to do it?

[Jeremy Tan]

So in short I need help with the sorry here

lemma forest_stacking (x : X) : stackSize (𝔘₃ (X := X) k n j) x ≤ C5_4_8 n := by
  have exum : ∀ u : 𝔘₃ k n j, ∃ m : 𝔐 (X := X) k n, smul 100 u.1 ≤ smul 1 m.1 := fun ⟨u, mu⟩ ↦ by
    replace mu := (𝔘₃_subset_𝔘₂.trans 𝔘₂_subset_𝔘₁ |>.trans 𝔘₁_subset_ℭ₁) mu
    rw [ℭ₁, mem_diff, preℭ₁, mem_setOf, filter_mem_univ_eq_toFinset] at mu
    replace mu := (show 0 < 2 ^ j by positivity).trans_le mu.1.2
    rw [Finset.card_pos] at mu; obtain ⟨m, hm⟩ := mu
    rw [mem_toFinset, 𝔅, mem_setOf] at hm; exact ⟨⟨m, hm.1⟩, hm.2⟩
  let mf : 𝔘₃ k n j → 𝔐 (X := X) k n := fun u ↦ (exum u).choose
  have mfinj : Injective mf := by
    by_contra h; rw [not_injective_iff] at h; obtain ⟨u, u', mfe, neq⟩ := h; set m := mf u
    have iu : smul 100 u.1 ≤ smul 1 m.1 := (exum u).choose_spec
    have iu' : smul 100 u'.1 ≤ smul 1 m.1 := mfe ▸ (exum u').choose_spec
    have iu₂ : ball_{𝓘 m.1} (𝒬 m.1) 1 ⊆ ball_{𝓘 u.1} (𝒬 u.1) 100 := iu.2
    have iu'₂ : ball_{𝓘 m.1} (𝒬 m.1) 1 ⊆ ball_{𝓘 u'.1} (𝒬 u'.1) 100 := iu'.2
    have nd : ¬Disjoint (ball_{𝓘 u.1} (𝒬 u.1) 100) (ball_{𝓘 u'.1} (𝒬 u'.1) 100) := by
      rw [not_disjoint_iff]
      use 𝒬 m.1, iu₂ (mem_ball_self zero_lt_one), iu'₂ (mem_ball_self zero_lt_one)
    apply absurd _ nd
    sorry

[Jeremy Tan]

oh wait…

[Jeremy Tan]

yeah I think I've found a legitimate error in the proof of Lemma 5.4.9

[Jeremy Tan]

(5.1.14) requires 𝓘 u < 𝓘 u' or 𝓘 u' < 𝓘 u (strict containment), but (2.0.8) only allows us to conclude weak containment 𝓘 u ≤ 𝓘 u' or 𝓘 u' ≤ 𝓘 u. What if 𝓘 u = 𝓘 u'?

[Jeremy Tan]

All that I've been able to conclude in that case is Disjoint (Ω u) (Ω u'), not the disjointness of the 100-radius balls needed

[Floris van Doorn]

Jeremy Tan said:

yeah I think I've found a legitimate error in the proof of Lemma 5.4.9

There is indeed a gap here. We're discussing a fix.

[Floris van Doorn]

There is a step missing in the blueprint, but from the proof of Lemma 5.4.2 you can separate out a lemma that if the 100-balls of u and u' intersect, then u ~ u'. This shows that if u is not related to u', then 𝓘 u does not equal 𝓘 u' (and distinct elements in U_3 are not related).

[Floris van Doorn]

Edward van de Meent said:

i've run into another issue in 4.0.1. For property 2.0.11, the blueprint says to use lemma 4.1.9. this only covers the case where $t < 1$, and it's not clear (to me) that in the remaining case (with $1 \leq t$) the statement is true?

From Christoph: On the left hand side there is a subset of I, hence the LHS is at most mu(I).
If t>1, then the right hand side is larger than mu(I) and the statement is trivial

[Edward van de Meent]

ah, thanks!

[Edward van de Meent]

i'm currently merging master; if all goes well, i can start PRing the rest of 4.1 and 4.0.1. i do expect that the lean proofs can be optimized a decent amount, but i think that's something for later.

[Edward van de Meent]

for now i've thrown it all into one PR: #82. However, i imagine it is quite too large to review/merge at once; advice on how to split it is welcome.

[Floris van Doorn]

I'm going to use a different approach to reviewing here. Your proof compiles, and proves the correct thing, so I'm just going to merge it.
Anyone (especially you yourself) is encouraged to clean-up the proof / speed up the proof / factor out useful lemmas. But I think this can also be done after the merge.

[Pietro Monticone]

Floris van Doorn said:

I'm going to use a different approach to reviewing here. Your proof compiles, and proves the correct thing, so I'm just going to merge it.
Anyone (especially you yourself) is encouraged to clean-up the proof / speed up the proof / factor out useful lemmas. But I think this can also be done after the merge.

Done some of it here.

[Floris van Doorn]

I added 4 new tasks in the first post. These tasks combined finish chapter 5.

[Edward van de Meent]

i created a PR for adding the missing \lean and \leanok tags for chapter 4.1, at #86

[Jeremy Tan]

Another error found, this time in 5.4.8: in order to apply the URel transitivity you need to show u'' ∈ 𝔘₂ k n j, but you have only shown in the blueprint that u'' ∈ 𝔘₁ k n j (a weaker inclusion)

[Jeremy Tan]

oh wait

[James Sundstrom]

Claiming the lemmas about wnorm and MemWℒp. I didn't do the "optional: develop more API" part, so that's still available.

[Jim Portegies]

James Sundstrom said:

Claiming the lemmas about wnorm and MemWℒp. I didn't do the "optional: develop more API" part, so that's still available.

Hi James, can we briefly discuss? I'd like to understand a bit better what the current status is

[James Sundstrom]

I'm actually making the PR right now, it was a very easy task. (EDIT: Done)

[Floris van Doorn]

I added two new longer tasks to the list that together capture all of chapter 8.

[Jim Portegies]

@Floris van Doorn It turns out that the real interpolation theorem needs a version of Minkowski's theorem (namely Minkowski's integral inequality), that I cannot find in mathlib (the theorem that was linked in the original file points to the the Minkowsi inequality for the sum). Can I set out to prove Minkowski's integral inequality as part of proving the real interpolation theorem?

[Floris van Doorn]

Oh, good point.
Since the Real interpolation theorem is already such a big proof, it might be better to PR the statement of the Minkowski integral inequality so that someone can work on that in parallel. Does that sound good to you?

[Jim Portegies]

Floris van Doorn said:

it might be better to PR the statement of the Minkowski integral inequality so that someone can work on that in parallel.

That is fine too. I have made some thoughts on how to approach it (with some half baked work), so it may be nice to discuss with whoever is going to take it up. If only to hear how things can be done better :)