Outstanding Tasks, V1

Stream: Carleson

[Floris van Doorn]

There is a CONTRIBUTING file that contains some useful tips. (Some links only work after the current build has completed.)

Normal-sized tasks:

1. :check: (Edward van de Meent) Three simple lemmas about comparing volumes of balls w.r.t. a doubling measure: carleson#volume_ball_le_same, carleson#volume_ball_le_of_dist_le and carleson#volume_ball_le_of_subset. These are not explicitly in the blueprint, but will be needed for Lemma 4.1.1 and Lemma 4.1.2.
2. :check: (Jeremy Tan) Lemma 2.1.1 is a combinatorial lemma. I expect it is easiest to prove carleson#Θ.mk_le_of_le_dist first and then conclude carleson#Θ.card_le_of_le_dist and carleson#Θ.finite_of_le_dist from it.
3. :check: (Jeremy Tan) Lemma 2.1.2: two Lean lemmas about doing some approximations in a metric space.
4. :play: (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.
5. :check: (Jeremy Tan) A simple combinatorial lemma about balls covering other balls: carleson#CoveredByBalls.trans (used in Lemma 2.1.1)
6. :new: Lemma 4.0.3: this requires manipulating some integrals, and also require stating/proving that a bunch more things are integrable.
7. :new: 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.
8. :check: (Jeremy Tan) Show that 𝓓 X is almost a docs#SuccOrder: Define 𝓓.succ and prove the 4 lemmas below it.
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.
10. :check: (Bhavik Mehta) Prove Lemma 4.2.1 (simple exercise in a metric space)
11. :check: (Jeremy Tan) Prove Lemma 4.2.2 (short, but maybe a bit tricky to use the definitions Ω₁ and Ω₁_aux)
12. :check: (Jeremy Tan) Prove Lemma 4.2.3
13. :check: (Jeremy Tan) Prove Lemma 4.0.2 from the lemmas in Section 4.2 (quite long, but splits naturally into 5 parts).
14. :check: (Edward van de Meent) Prove lemma 4.1.1 and 4.1.2.
15. :check: (Jim Portegies) Proof basic properties about the distribution function carleson#MeasureTheory.distribution up to carleson#ContinuousLinearMap.distribution_le . This requires some simple measure theory. The proofs are in Folland, Real Analysis. section 6.3.
16. :check: (Mauricio Collares) (roughly already in Mathlib) Proof a more general layer-cake principle carleson#MeasureTheory.lintegral_norm_pow_eq_measure_lt which generalizes docs#MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul . Also please prove the three corollaries below. This is Lemma 9.0.1 in the blueprint.
17. :new: 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).

Large tasks. I will be splitting up these tasks into smaller subtasks, but feel free to already work on that. It is especially useful if you start by splitting it up by stating all definitions and lemmas.

• L1. :play: (Floris) Chapter 9 which proves Proposition 2.0.6: Vitali covering and the Hardy-Littlewood maximal equality. Some related things are already in Mathlib, like a special case of the layercake formula. Try to do this in Mathlib-generality, so that it can be added to Mathlib. The versions of the proposition we need for this project have already been stated.
• L2. Chapter 8: Hölder cancellative condition proving Proposition 2.0.5.
• L3. :play: (Edward van de Meent) Prove Lemma 4.0.1, the proof is in Section 4.1
• L4. :play: (Floris) Prove Lemma 4.0.2. The proof is in section 4.2 (this is now tasks 8-13).
• L5. Proposition 2.0.4 proven in chapter 7.
• L6. :play: (María Inés de Frutos Fernández) Proposition 2.0.3, proven in chapter 6.
• L7. :play: (Floris) Proposition 2.0.2, proven in chapter 5. Beware: We have found some mistakes in the lemmas in chapter 5, which need to be fixed. Some of these are pointed out in the source file for the blueprint
• L8. Prove Carleson's theorem for doubling metric measure spaces from the work done in chapters 4-9. This is done in chapter 3.
• L9. :play: (Leo Diedering) Derive the classical Carleson's theorem from the general version. This is done in chapter 10.
• 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.

[Edward van de Meent]

i'd like to try my hand at some of the lemmas in 4.1. for now i'd like to claim 4.1.1 and 4.1.2

[Terence Tao]

I wonder if there are some "quick win" goals that could be used as milestones for the project. I see that you already have the Hardy-Littlewood maximal inequality in there as an early milestone for instance. What about say Fejer's theorem for convergence of Cesaro averages of Fourier series - would that be something that could be integrated into the project? Or some of the other foundational results of Calderon-Zygmund theory? Or a general form of the Cotlar-Knapp-Stein lemma?

[Floris van Doorn]

Oh, there are definitely some much simpler things we could proof first, along the way, even if they are not strictly needed for the final result. I'm happy to incorporate them to this project as well (although anyone working on them can just as well directly put it into Mathlib)
I have a separate project where I'm doing some more basic Fourier analysis with some students: https://github.com/fpvandoorn/BonnAnalysis/
That project is mostly to try to formalize interpolation theorems. The real (Marcinkiewicz) interpolation theorem will also be useful for the proof here.

[Jeremy Tan]

I'm going to try my hand at 2.1.1 and 5.3.4

[Jeremy Tan]

but how can I actually get 1.0.11 from ProofData? It's an instance so I had to name it

[Ruben Van de Velde]

I had a look at 3. Lemma 2.1.2. I was wondering if it's true that (I : Set X) = (J : Set X) implies I = J?

[Edward van de Meent]

I think so, if the coercion is via a SetLike instance

[Ruben Van de Velde]

It's not, it's just a plain coercion: http://florisvandoorn.com/carleson/docs/Carleson/GridStructure.html#instCoe%F0%9D%93%93Set

[Edward van de Meent]

then, from what i can tell, no. i can imagine that it would be nice to have though

[Ruben Van de Velde]

My question was whether it was true, not if it had been formalized yet

[Vincent Beffara]

Wouldn't it be equivalent to saying that GridStructure.coe𝓓 is injective?

[Edward van de Meent]

it would. which would be exactly the last field needed for a SetLike instance.
From the comment in the declaration of GridStructure, i believe it is something that can safely be assumed.

[Vincent Beffara]

From what I understand (just discovering the code), it does not follow from the assumptions that are already present but can be safely added to the structure.

[Edward van de Meent]

yes, exactly

[Vincent Beffara]

Unless later in proofs, what is really needed is the injectivity of the map from i to (coe𝓓 i, s i, c i) but for some reason it is useful to have the same set occur at two different scales, or with a different marked center.

[Jeremy Tan]

Never mind, I retract my prior claim

[Floris van Doorn]

It is indeed intended that GridStructure.coe𝓓 is injective. I just added that hypothesis to the structure. Thanks for the correction.
Note: when s i ≠ s j then you can already conclude that coe𝓓 i ≠ coe𝓓 j, by ball_subset_𝓓 and 𝓓_subset_ball (for D > 16, which we will assume)

[Floris van Doorn]

I have split task L4 into 6 smaller tasks: 8-13. There are plenty of tasks for anyone :smile:

[Bhavik Mehta]

Jeremy Tan said:

Never mind, I retract my prior claim

To clarify, does this mean you're unclaiming 2.1.1 and 5.3.4, or is there another claim?

[Jeremy Tan]

Actually, scrap that. I'll go ahead anyway, nothing is retracted

[Jeremy Tan]

My first concern though is how to get the blueprint properties in Lean

[Floris van Doorn]

What do you mean by that? You can get the properties out of ProofData just by using the field names, e.g.

  have : 4 ≤ a := four_le_a X

[Jeremy Tan]

1.0.11 doesn't seem to have such a field name associated to it, but it's 1am here

[Floris van Doorn]

1.0.11 is CompatibleFunctions.ballsCoverBalls

[Jeremy Tan]

OK, I think the proof of 2.1.1 is wrong

[Jeremy Tan]

If I apply 1.0.11 $k$ times with

have pmul := BallsCoverBalls.pow_mul (k := k) (r := r) fun r ↦
    CompatibleFunctions.ballsCoverBalls (x := x₀) (r := R) (R := r)

I only get that the large ball is covered by $2^{ka}$ balls of radius r, not r / 2

[Jeremy Tan]

Yes 2.1.1 is wrong as stated

[Floris van Doorn]

You are correct, k should be replaced by k+1 in the conclusion.

[Vincent Beffara]

Floris van Doorn said:

It is indeed intended that GridStructure.coe𝓓 is injective. I just added that hypothesis to the structure. Thanks for the correction.
Note: when s i ≠ s j then you can already conclude that coe𝓓 i ≠ coe𝓓 j, by ball_subset_𝓓 and 𝓓_subset_ball (for D > 16, which we will assume)

Ah indeed I was missing the assumption that D > 16. BTW why did you choose this representation with a family indexed by an embedded type 𝓓 rather than something like this?

variable (X) in
structure tile (D : ℝ) where
  toSet : Set X
  s : ℤ
  c : X
  ball_subset : ball c (D ^ s / 4) ⊆ toSet
  subset_ball : toSet ⊆ ball c (4 * D ^ s)

variable (X) in
class GridStructure' (D κ : outParam ℝ) (S : outParam ℤ) (o : outParam X) where
  𝓓 : Finset (tile X D)
  range_s_subset : ∀ D ∈ 𝓓, D.s ∈ Icc (-S) S
  -- ... the other properties

[Bhavik Mehta]

I'd like to claim 9 and 10

[Bhavik Mehta]

I've made a PR for 10, but 9 is heavily dependent on the precise form that 2.1.1 comes out as, so I'll wait on Jeremy for that to be completed.

[Bhavik Mehta]

lemma large_dist_of_disjoint_balls {z z' : Θ X} {x₀ R}
    (h : Disjoint (ball_{x₀, R} z C𝓩) (ball_{x₀, R} z' C𝓩)) : 2 * C𝓩 ≤ dist_{x₀, R} z z' :=
  sorry

This statement would be useful for the construction of 𝓩 - is it true? (In particular, I think this is used implicitly when proving the finiteness bound on sets satisfying 4.2.1 and 4.2.2

[Floris van Doorn]

@Vincent Beffara There are two differences in your approach:
(1) bundle every cube in the grid into one structure
(2) Use a Finset instead of an indexing Fintype.

I must say I didn't do an exhaustive comparison between different representations, and maybe your representation is better. I generally like to work with (indexed) families of objects compared to collections (i.e. a (fin)set), but packaging the elements into a structure might be a good idea...

[Floris van Doorn]

(a note on terminology: elements in 𝓓 are called cubes, we also have a TileStructure whose inhabitants are called tiles)

[Floris van Doorn]

Bhavik Mehta said:

I've made a PR for 10, but 9 is heavily dependent on the precise form that 2.1.1 comes out as, so I'll wait on Jeremy for that to be completed.

If it helps, I just separated out the constant that appears in Lemma 2.1.1. Feel free to work on task 9 using that constant. But maybe you are wondering about the rest of the formulation.

[Floris van Doorn]

@Jeremy Tan I fixed the constant for Lemma 2.1.1 in the Lean formalization

[Floris van Doorn]

Bhavik Mehta said:

lemma large_dist_of_disjoint_balls {z z' : Θ X} {x₀ R}
    (h : Disjoint (ball_{x₀, R} z C𝓩) (ball_{x₀, R} z' C𝓩)) : 2 * C𝓩 ≤ dist_{x₀, R} z z' :=
  sorry

This statement would be useful for the construction of 𝓩 - is it true? (In particular, I think this is used implicitly when proving the finiteness bound on sets satisfying 4.2.1 and 4.2.2

Oh, good question. That doesn't hold in arbitrary metric spaces... Let me think about it (I will see Christoph Thiele tomorrow, so I can also ask him if I don't figure it out).

[Floris van Doorn]

I think it doesn't hold as currently stated. But the main usage for the distance is the local oscillation (LHS of (1.0.7)), and so we can probably assume that the distance comes from a seminorm...

[Bhavik Mehta]

I see - I'll leave that as a sorry for now and continue?

[Bhavik Mehta]

If you are thinking about this already - it may alternatively be the case that this isn't needed for \MCZ, but I think something like it is necessary to transfer from eqn 4.2.2 to something satisfying the preconditions of Lemma 2.1.1. An alternative approach is to note that the proof of Lemma 2.1.1 doesn't need that the distance is large, only that certain balls intersect with Z in limited capacity; so maybe 2.1.1 can be strengthened by relaxing that hypothesis?

[Floris van Doorn]

Those are good points. This problem might indeed be fixed by strengthening 2.1.1, but I'll discuss it tomorrow, because it might still lead to problems elsewhere.

[Bhavik Mehta]

Things like lower-secant-bound and dirichlet-kernel are marked as green on the blueprint but they don't seem to have attached Lean declarations or proofs. Are these available somewhere?

[Floris van Doorn]

Bhavik Mehta said:

Things like lower-secant-bound and dirichlet-kernel are marked as green on the blueprint but they don't seem to have attached Lean declarations or proofs. Are these available somewhere?

Good point. @Leo Diedering, could you add \lean{} commands to every result of chapter 10 that you've stated already in Lean?

[Pietro Monticone]

Opened PR adding missing \lean{} placeholders and filling some of them (e.g. lower-secant-bound, but not dirichlet-kernel because I'm not sure if it's supposed to take multiple declarations as arguments).

[Jeremy Tan]

@Floris van Doorn so I've completed almost all the proof for 2.1.1, except...

lemma Θ.finite_and_mk_le_of_le_dist {x₀ : X} {r R : ℝ} (hr : 0 < r) {f : Θ X} {k : ℕ}
    {𝓩 : Set (Θ X)} (h𝓩 : 𝓩 ⊆ ball_{x₀, R} f (r * 2 ^ k))
    (h2𝓩 : ∀ z z', z ∈ 𝓩 → z' ∈ 𝓩 → z ≠ z' → r ≤ dist_{x₀, R} z z') :
    𝓩.Finite ∧ Cardinal.mk 𝓩 ≤ C2_1_1 k a := by
  have pmul := (BallsCoverBalls.pow_mul (k := k + 1) (r := r / 2) fun r ↦
    CompatibleFunctions.ballsCoverBalls (x := x₀) (r := R) (R := r)) f
  rw [show 2 ^ (k + 1) * (r / 2) = r * 2 ^ k by ring, coveredByBalls_iff] at pmul
  obtain ⟨𝓩', c𝓩', u𝓩'⟩ := pmul
  classical
    let g : Θ X → Finset (Θ X) := fun z ↦ 𝓩'.filter (z ∈ ball_{x₀, R} · (r / 2))
    have g_pd : 𝓩.PairwiseDisjoint g := fun z hz z' hz' hne ↦ by
      refine Finset.disjoint_filter.mpr fun c hc mz mz' ↦ ?_
      simp_rw [mem_ball] at mz mz'
      have := (dist_triangle_right (α := WithFunctionDistance x₀ R) ..).trans_lt
        (add_lt_add_of_lt_of_lt mz mz')
      rw [add_halves, lt_iff_not_le] at this
      exact absurd (h2𝓩 z z' hz hz' hne) this
  have g_ne : ∀ z, z ∈ 𝓩 → (g z).Nonempty := fun z hz ↦ by
    obtain ⟨c, hc⟩ := mem_iUnion.mp <| mem_of_mem_of_subset hz (h𝓩.trans u𝓩')
    simp only [mem_iUnion, exists_prop] at hc
    use c; simpa only [g, Finset.mem_filter]
  have g_injOn : 𝓩.InjOn g := fun z hz z' hz' e ↦ by
    have : z ≠ z' → Disjoint (g z) (g z') := g_pd hz hz'
    rw [← e, Finset.disjoint_self_iff_empty] at this
    exact not_ne_iff.mp <| this.mt <| Finset.nonempty_iff_ne_empty.mp (g_ne z hz)
  have g_subset : g '' 𝓩 ⊆ 𝓩'.powerset.toSet := fun gz hgz ↦ by
    rw [mem_image] at hgz
    obtain ⟨z, hz⟩ := hgz
    simp_rw [Finset.coe_powerset, mem_preimage, mem_powerset_iff, Finset.coe_subset, ← hz.2, g,
      Finset.filter_subset]
  have f𝓩 : (g '' 𝓩).Finite := Finite.subset 𝓩'.powerset.finite_toSet g_subset
  rw [Set.finite_image_iff g_injOn] at f𝓩
  refine ⟨f𝓩, ?_⟩
  lift 𝓩 to Finset (Θ X) using f𝓩
  simp_rw [Cardinal.mk_fintype, Finset.coe_sort_coe, Fintype.card_coe]
  norm_cast
  classical calc
    _ = ∑ u ∈ 𝓩, 1 := by simp
    _ ≤ ∑ u ∈ 𝓩, (g u).card := Finset.sum_le_sum fun z hz ↦ Finset.card_pos.mpr (g_ne z hz)
    _ = (𝓩.biUnion g).card := (Finset.card_biUnion (fun z hz z' hz' ↦ g_pd hz hz')).symm
    _ ≤ 𝓩'.card := by
      refine Finset.card_le_card fun _ h ↦ ?_
      rw [Finset.mem_biUnion] at h
      exact Finset.mem_of_subset (by simp [g]) h.choose_spec.2
    _ ≤ ⌊2 ^ a⌋₊ ^ (k + 1) := c𝓩'
    _ ≤ _ := by
      rw [C2_1_1, mul_comm, pow_mul]
      apply pow_le_pow_left'
      -- ⌊2 ^ a⌋₊ ≤ 2 ^ ⌊a⌋₊ - FALSE (take e.g. a = 1.9)
      sorry

[Jeremy Tan]

At the end of it all it reduces to ⌊2 ^ a⌋₊ ≤ 2 ^ ⌊a⌋₊, but that is false – indeed the reverse inequality is true

[Jeremy Tan]

can I commit this straight to your repo or do you need to give me permission first?

[Jeremy Tan]

But if the constant is 2 ^ ((k + 1) * (⌊a⌋₊ + 1)) it works

[Edward van de Meent]

is there a reason why the doubling in DoublingMeasure is about volume.real rather than volume itself?

[Edward van de Meent]

because i find myself rather using the latter

[Yaël Dillies]

Jeremy Tan said:

can I commit this straight to your repo or do you need to give me permission first?

Note that you can always open a PR

[Bhavik Mehta]

(deleted)

[Mauricio Collares]

Jeremy Tan said:

At the end of it all it reduces to ⌊2 ^ a⌋₊ ≤ 2 ^ ⌊a⌋₊, but that is false – indeed the reverse inequality is true

In the blueprint, a is a natural number. I suspect it became of type ℝ in the formalization to avoid a few casts, which led to unintended side effects.

[Floris van Doorn]

Mauricio Collares said:

Jeremy Tan said:

At the end of it all it reduces to ⌊2 ^ a⌋₊ ≤ 2 ^ ⌊a⌋₊, but that is false – indeed the reverse inequality is true

In the blueprint, a is a natural number. I suspect it became of type ℝ in the formalization to avoid a few casts, which led to unintended side effects.

This is exactly what happened. We're mostly using a as a real number, but then I put the floor in the wrong place.

@Jeremy Tan Thank you for the proof! Can you replace the constant by 2 ^ ((k + 1) * ⌈a⌉₊)?

[Floris van Doorn]

Edward van de Meent said:

is there a reason why the doubling in DoublingMeasure is about volume.real rather than volume itself?

When starting on this project I was hoping to stay in Real as much as possible. However, that turned out to be less convenient than I hoped.
Please add the ENNReal inequality as a lemma

[Terence Tao]

For what it's worth, the PFR project developed some API for Real-valued measures rather than ENNReal-valued measures, see https://teorth.github.io/pfr/docs/PFR/ForMathlib/MeasureReal.html . In principle this is supposed to go into Mathlib eventually, but that's a low priority right now. But I guess you could import it here if it would be a net help.

[Jeremy Tan]

Floris van Doorn said:

Can you replace the constant by 2 ^ ((k + 1) * ⌈a⌉₊)?

def C2_1_1 (k : ℕ) (a : ℝ) : ℕ := 2 ^ ((k + 1) * ⌈a⌉₊) -- todo: fix in blueprint

-- Note: See also/prove card_le_of_le_dist in DoublingMeasure.
lemma Θ.finite_and_mk_le_of_le_dist {x₀ : X} {r R : ℝ} {f : Θ X} {k : ℕ}
    {𝓩 : Set (Θ X)} (h𝓩 : 𝓩 ⊆ ball_{x₀, R} f (r * 2 ^ k))
    (h2𝓩 : ∀ z z', z ∈ 𝓩 → z' ∈ 𝓩 → z ≠ z' → r ≤ dist_{x₀, R} z z') :
    𝓩.Finite ∧ Cardinal.mk 𝓩 ≤ C2_1_1 k a := by
  have pmul := (BallsCoverBalls.pow_mul (k := k + 1) (r := r / 2) fun r ↦
    CompatibleFunctions.ballsCoverBalls (x := x₀) (r := R) (R := r)) f
  rw [show 2 ^ (k + 1) * (r / 2) = r * 2 ^ k by ring, coveredByBalls_iff] at pmul
  obtain ⟨𝓩', c𝓩', u𝓩'⟩ := pmul
  classical
    let g : Θ X → Finset (Θ X) := fun z ↦ 𝓩'.filter (z ∈ ball_{x₀, R} · (r / 2))
    have g_pd : 𝓩.PairwiseDisjoint g := fun z hz z' hz' hne ↦ by
      refine Finset.disjoint_filter.mpr fun c _ mz mz' ↦ ?_
      simp_rw [mem_ball] at mz mz'
      have := (dist_triangle_right (α := WithFunctionDistance x₀ R) ..).trans_lt
        (add_lt_add_of_lt_of_lt mz mz')
      rw [add_halves, lt_iff_not_le] at this
      exact absurd (h2𝓩 z z' hz hz' hne) this
  have g_ne : ∀ z, z ∈ 𝓩 → (g z).Nonempty := fun z hz ↦ by
    obtain ⟨c, hc⟩ := mem_iUnion.mp <| mem_of_mem_of_subset hz (h𝓩.trans u𝓩')
    simp only [mem_iUnion, exists_prop] at hc
    use c; simpa only [g, Finset.mem_filter]
  have g_injOn : 𝓩.InjOn g := fun z hz z' hz' e ↦ by
    have : z ≠ z' → Disjoint (g z) (g z') := g_pd hz hz'
    rw [← e, Finset.disjoint_self_iff_empty] at this
    exact not_ne_iff.mp <| this.mt <| Finset.nonempty_iff_ne_empty.mp (g_ne z hz)
  have g_subset : g '' 𝓩 ⊆ 𝓩'.powerset.toSet := fun gz hgz ↦ by
    rw [mem_image] at hgz
    obtain ⟨z, hz⟩ := hgz
    simp_rw [Finset.coe_powerset, mem_preimage, mem_powerset_iff, Finset.coe_subset, ← hz.2, g,
      Finset.filter_subset]
  have f𝓩 : (g '' 𝓩).Finite := Finite.subset 𝓩'.powerset.finite_toSet g_subset
  rw [Set.finite_image_iff g_injOn] at f𝓩
  refine ⟨f𝓩, ?_⟩
  lift 𝓩 to Finset (Θ X) using f𝓩
  simp_rw [Cardinal.mk_fintype, Finset.coe_sort_coe, Fintype.card_coe]
  norm_cast
  classical calc
    _ = ∑ _ ∈ 𝓩, 1 := by simp
    _ ≤ ∑ u ∈ 𝓩, (g u).card := Finset.sum_le_sum fun z hz ↦ Finset.card_pos.mpr (g_ne z hz)
    _ = (𝓩.biUnion g).card := (Finset.card_biUnion (fun z hz z' hz' ↦ g_pd hz hz')).symm
    _ ≤ 𝓩'.card := by
      refine Finset.card_le_card fun _ h ↦ ?_
      rw [Finset.mem_biUnion] at h
      exact Finset.mem_of_subset (by simp [g]) h.choose_spec.2
    _ ≤ ⌊2 ^ a⌋₊ ^ (k + 1) := c𝓩'
    _ ≤ _ := by
      rw [C2_1_1, mul_comm, pow_mul]
      apply pow_le_pow_left'
      exact_mod_cast (Nat.floor_le (by positivity)).trans
        (Real.rpow_le_rpow_of_exponent_le one_le_two (Nat.le_ceil a))

[Jeremy Tan]

I have now proved normal-sized task 5 from the list:

lemma CoveredByBalls.trans (h : CoveredByBalls s n r)
    (h2 : BallsCoverBalls X r r' m) : CoveredByBalls s (n * m) r' := by
  obtain ⟨b0, hb0, hs0⟩ := h
  rw [coveredByBalls_iff]
  have := fun x ↦ ((coveredByBalls_iff ..).mp (h2 x))
  classical
    use b0.biUnion fun x ↦ (this x).choose
    refine ⟨?_, fun p hp ↦ ?_⟩
    · calc
        _ ≤ ∑ x ∈ b0, (this x).choose.card := card_biUnion_le ..
        _ ≤ ∑ _ ∈ b0, m := sum_le_sum fun x _ ↦ (this x).choose_spec.1
        _ ≤ _ := by
          rw [sum_const_nat fun x ↦ congrFun rfl]
          exact Nat.mul_le_mul_right m hb0
    · obtain ⟨b, _, hb⟩ := Set.mem_iUnion₂.mp (hs0 hp)
      have tmp := ((this b).choose_spec.2) hb
      rw [Set.mem_iUnion₂] at tmp ⊢
      obtain ⟨c, _, hc⟩ := tmp
      use c, (by rw [mem_biUnion]; use b), hc

[Floris van Doorn]

Terence Tao said:

For what it's worth, the PFR project developed some API for Real-valued measures rather than ENNReal-valued measures, see https://teorth.github.io/pfr/docs/PFR/ForMathlib/MeasureReal.html . In principle this is supposed to go into Mathlib eventually, but that's a low priority right now. But I guess you could import it here if it would be a net help.

Yes, I'm using the same code in this project, though good old-fashioned copy-paste.

[Floris van Doorn]

@Jeremy Tan Thanks! Please open pull requests with these lemmas.

[Jeremy Tan]

but CONTRIBUTING.md says

To publish your changes on Github, you need to be added as a contributor to this repository. Make a Github account if you don't have one already and send your Github account per email to Floris. I will add you.

so do I have to be added as a contributor first?

[Kim Morrison]

That is probably just wrong, and you can make a PR from a fork?

[Jeremy Tan]

@Kim Morrison :squared_ok: https://github.com/fpvandoorn/carleson/pull/38

[Floris van Doorn]

@Jeremy Tan Thanks for pointing that out. Those are old instructions when there were only a few contributors. Now I think switching to a pull-request model is better. I changed the README file. And thanks for your pull request!

[Floris van Doorn]

Georges Gonthier is carefully reading the blueprint, and found two simplifications:
(1) @Bhavik Mehta: We should be able to define 𝓩 to be a subset of range Q (and then 𝓩_subset is reformulated as only covering range Q). This has two advantages:

• It simplifies the finiteness condition: it is a subset of a finite set
• We then get that range 𝒬 ⊆ range Q, which should simplify/fix proofs elsewhere.
  PS: I'm quite sure we don't need maximal_𝓩_card, only maximal_𝓩.

(2) @Pietro Monticone We're probably changing the construction of the grid structure a little bit so that there is only 1 tile at level S with center o (then we might not cover all of ball o (D ^ S), but should be able to cover the ball with half the radius, which is good enough). This will simplify proofs elsewhere.

[Bhavik Mehta]

Ah, only covering range Q is super helpful, thanks for pointing that out!

[Edward van de Meent]

i've finished 4.1.1 and 4.1.2, and made a PR.
I don't know how to work the blueprint though, so those changes aren't included

[Floris van Doorn]

Edward van de Meent said:

i've finished 4.1.1 and 4.1.2, and made a PR.
I don't know how to work the blueprint though, so those changes aren't included

Great, thanks! I'll make the changes to the blueprint after I merge your PR.

[Edward van de Meent]

i believe i've gone through all comments on the PR, and it's ready for another review

[Edward van de Meent]

ah, i see it's been merged :tada:

[Edward van de Meent]

i'd like to claim 4.1.3 please

[Floris van Doorn]

@Pietro Monticone is also planning to work further section 4.1 (see top post here, task L3). Can you coordinate with him that you're not doing double work?

[Edward van de Meent]

ah yes, good point...

[Edward van de Meent]

i'm currently mostly concerned with getting good defs for I1, I2, ...

[Pietro Monticone]

I'm sorry I've not been fast enough. I am currently very busy with my exams over the next few weeks.

[Floris van Doorn]

Important Note: the definition of carleson#GridStructure and carleson#TileStructure just changed, both in Lean and in the blueprint. A GridStructure now has a (unique) maximal element. For a tile structure, we added the condition range 𝒬 ⊆ range Q.
They now have slightly stronger conditions, but the constructions in chapter 4 should be adapted accordingly.
This means that some proofs in chapter 6 will become simpler (this is not yet incorporated in the blueprint).

[Floris van Doorn]

Don't worry @Pietro Monticone. I understand that everyone only has limited time for this project.
If you prefer, Edward can continue on Section 4, and then I'll find another not-analysis-heavy task for you later.

[Pietro Monticone]

Floris van Doorn said:

Don't worry Pietro Monticone. I understand that everyone only has limited time for this project.
If you prefer, Edward can continue on Section 4, and then I'll find another not-analysis-heavy task for you later.

Sounds good to me.

[Floris van Doorn]

I added three tasks 15-17 towards the real interpolation theorem. If someone wants a bigger project (but still a lot smaller than a whole chapter of the blueprint) that requires a lot of intergral manipulations, feel free to claim task L10, to prove the real interpolation theorem itself.

[Jim Portegies]

Floris van Doorn said:

I added three tasks 15-17 towards the real interpolation theorem. If someone wants a bigger project (but still a lot smaller than a whole chapter of the blueprint) that requires a lot of intergral manipulations, feel free to claim task L10, to prove the real interpolation theorem itself.

Hi all, I'm relatively new to lean (but do have some experience with CoQ), I'd love to contribute. Could task 15 be a good place to start?

[Johan Commelin]

Hi @Jim Portegies, welcome! Great to see you here :smiley:

[Floris van Doorn]

Welcome! Yes, I think task 15 is a good starter task! I think a significant part will be to find the relevant lemmas in the library (e.g. docs#MeasureTheory.measure_union_le ).

[Jim Portegies]

Perfect! Could I work on task 15 then?

[Floris van Doorn]

Yes, I added you to the list!

[Floris van Doorn]

Floris van Doorn said:

It is indeed intended that GridStructure.coe𝓓 is injective. I just added that hypothesis to the structure. Thanks for the correction.
Note: when s i ≠ s j then you can already conclude that coe𝓓 i ≠ coe𝓓 j, by ball_subset_𝓓 and 𝓓_subset_ball (for D > 16, which we will assume)

@Edward van de Meent I take back what I said above. My argument is invalid.
It is true that if s i = s j + 1 then coe𝓓 j ⊆ ball (c j) R₁ ⊆ ball (c i) R₂ ⊆ coe𝓓 i with R₂ > 2^1596 * R₁. However, that doesn't actually imply that ball (c i) R₂ is strictly larger than ball (c j) R₁, since we're just in an (somewhat) arbitrary metric space. I will remove the injectivity of coe𝓓 later. The pair (coe𝓓, s) will be injective.
This might require some precision on the formulation of some lemmas.

[Floris van Doorn]

Ok, I pushed this change. Whenever you see I ⊆ J you should probably translate it to I ≤ J. Lean now has both notions on 𝓓 X, but they're not equivalent. (≤ is stronger)

[Jeremy Tan]

4.2.2 and 4.2.3 are done https://github.com/fpvandoorn/carleson/pull/43

[Floris van Doorn]

That's great! Thanks! Are you planning to continue on Lemma 4.0.2? No pressure, but if you are, then I'll add your name to it so that nobody else claims it.

[Jeremy Tan]

I think I'm going to continue on 4.0.2, but already the maths is getting very complicated

[Mauricio Collares]

Can I try my hand at Lemma 9.0.1 (carleson#MeasureTheory.lintegral_norm_pow_eq_measure_lt)?

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

Floris van Doorn said:

This means that some proofs in chapter 6 will become simpler (this is not yet incorporated in the blueprint).

Does this apply to any of the proofs in Section 6.1?

[Floris van Doorn]

My understanding is that this commit did these simplifications, so they should be live now. It seems that Section 6.1 was not touched.
It is possible that there are still some roundabout arguments. The refactor allows us to conclude from IsMax i that i = topCube. Before there were a few case distinctions when reasoning about these maximal cubes/top cubes.

[Jeremy Tan]

Second part of tile existence lemma is now done https://github.com/fpvandoorn/carleson/pull/44

[Jeremy Tan]

but man that was insanely tough

[Floris van Doorn]

Great! Thanks!

[Jeremy Tan]

I cannot follow the argument here. Shouldn't it be "Thus, by (4.2.3), there exists z' ∈ \mathcal{Z}(I) with x ∈ B_{I°}(z', 0.7)", and similarly for the inclusion after that?

image.png

[Jeremy Tan]

If this step is correct I don't see how Equation (4.2.3) justifies it

[Jeremy Tan]

(https://github.com/fpvandoorn/carleson/pull/46)

[Jeremy Tan]

The proof seems to imply that Q(x) = ϑ

[Jeremy Tan]

Floris van Doorn said:

I will remove the injectivity of coe𝓓 later. The pair (coe𝓓, s) will be injective.
This might require some precision on the formulation of some lemmas.

I'm going to need the injectivity of coe𝓓 proper in proving tile existence, otherwise I can't prove I = J that is one of the steps in proving relative_fundamental_dyadic

[Floris van Doorn]

Oh, you indeed couldn't prove I = J, since relative_fundamental_dyadic was still written using ⊆ instead of ≤. I fixed that now, and removed the subset notation on 𝓓 X altogether, so that we are unlikely to make that mistake again.
Are you now able to prove I = J using the stronger hypothesis in relative_fundamental_dyadic? Note that you can apply le_antisymm for ≤ on 𝓓 X.
I'm afraid that we cannot assume injectivity of coe𝓓.

[Jeremy Tan]

Floris van Doorn said:

Oh, you indeed couldn't prove I = J, since relative_fundamental_dyadic was still written using ⊆ instead of ≤. I fixed that now, and removed the subset notation on 𝓓 X altogether, so that we are unlikely to make that mistake again.
Are you now able to prove I = J using the stronger hypothesis in relative_fundamental_dyadic? Note that you can apply le_antisymm for ≤ on 𝓓 X.
I'm afraid that we cannot assume injectivity of coe𝓓.

Done.

[Jeremy Tan]

@Floris van Doorn :up_button:

[Mauricio Collares]

Mauricio Collares said:

Can I try my hand at Lemma 9.0.1 (carleson#MeasureTheory.lintegral_norm_pow_eq_measure_lt)?

I just noticed that this is a lot closer to something in Mathlib than I expected (namely docs#MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul), which makes it a little less fun. I can do it on Monday if it's still useful, though.

[Floris van Doorn]

@Mauricio: Oh! I didn't know we had another file with applications of the layercake principle. Then it's indeed a very small task. I don't know precisely what form we need, so probably Mathlib's version is good enough.

@Jeremy: I don't have time to look at your remaining questions/PR today, I'll come back to you a bit later. Sorry.

[Jeremy Tan]

@Floris van Doorn well I've solved all my queries. There were some non sequitur steps in the blueprint that I've excised

[Jeremy Tan]

I have now proved the entire tile existence lemma at https://github.com/fpvandoorn/carleson/pull/46

[Jeremy Tan]

I have now completed task 8 in the outstanding tasks list: https://github.com/fpvandoorn/carleson/pull/47

[Jeremy Tan]

(note that PR #47 shuffles the positions/names of some lemmas used in PR #46, so PR #47 must be merged first)

[Jim Portegies]

@Floris van Doorn I have just created a PR for task 15. The proof for lemma continuousWithinAt_distribution is very long. I've started exploring a different route too (not included in the PR), that would use a neighborhood basis that would work for every point in ENNReal, however the proof that that is really a neighborhood basis seems to get out of hand. The problem is mostly with case distinction and the fact that I don't know how to do computations conveniently in ENNReal.

[Jeremy Tan]

Jeremy Tan said:

(note that PR #47 shuffles the positions/names of some lemmas used in PR #46, so PR #47 must be merged first)

Actually, scrap that. #46 now includes #47

[Jeremy Tan]

@Floris van Doorn did you see my completed PRs?

[Edward van de Meent]

does the blueprint look weird for anyone else?
image.png

[Jeremy Tan]

Floris needs to clear the cache again

[Floris van Doorn]

Yes, I'm trying to fix CI (and move to the proper leanblueprint infrastructure), and I'm having some issues...

[Floris van Doorn]

@Jeremy Tan Yes, I've seen them, but I've been fighting with the CI for the last few hours.

[Floris van Doorn]

Okay, it will stay broken for a while. I'm out of energy to fix this.

[Jeremy Tan]

@Floris van Doorn your latest commit did work, and the dependency graph is working again

[Jim Portegies]

Would it be okay if I start working towards the real interpolation theorem, task L.10?

[Floris van Doorn]

Yes, that would be amazing!

[James Sundstrom]

@Floris van Doorn I was looking at 2.1.3 and Psi.lean defines Ks using K x y * ψ (D ^ s * dist x y), whereas the blueprint uses D^(-s). At a quick glance, it looks like all other occurrences of -s are swapped with s appropriately, so this is a different choice of convention rather than a single typo. I haven't spent enough time with this to know which one would be easier to change.

[Floris van Doorn]

Please change the formalization, and use the convention from the blueprint. The blueprint was updated at some point (probably including this change), and it will be easier to use that throughout.

[Floris van Doorn]

Shall I put your name on that item?

[James Sundstrom]

Sure, I'll give it a shot.