Equation (5.3.3)

Stream: Carleson

[Jeremy Tan]

I am convinced that equation (5.3.3), the first part of Lemma 5.3.3, is false

[Jeremy Tan]

" $\mathfrak q\le \mathfrak q'$ and $\lambda \ge 1.1 \implies \lambda \mathfrak q \lesssim \mathfrak q'$ "– the second part of the definition of $\lesssim$ means that a ball of radius $\lambda r$ is contained in a ball of the same radius, which can only happen if the balls have the same centres. This is clearly not true in general

[Edward van de Meent]

at first glance it looks like it's 5.3.1 with specified values $n,m=1$ and $n',m'=\lambda$?

[Jeremy Tan]

no, the hypothesis isn't $\mathfrak q\lesssim\mathfrak q'$, only $\mathfrak q\le\mathfrak q'$ which is different

[Edward van de Meent]

ah, i see... and then i'm guessing that one doesn't imply the other? but it seemingly should?

[Jeremy Tan]

Here are the definitions of $\le$ and $\lesssim$

image.png

[Edward van de Meent]

could it be a typo in 5.3.3?

[Jeremy Tan]

Also, Lemma 5.3.3 is only used in Lemma 5.4.1, and that lemma only uses Equation (5.3.4) of Lemma 5.3.3

[Jeremy Tan]

So yes, I'm guessing there is a typo in @Floris van Doorn's blueprint and that indeed Equations (5.3.3), (5.3.5) can just be done away with

[Jeremy Tan]

All of this is in https://github.com/fpvandoorn/carleson/pull/50

[Jeremy Tan]

(sorry Ruben, you claimed 2.1.2 but didn't get back with anything for a few days…)

[Jeremy Tan]

wait, Equation (5.3.3) is used elsewhere, I was relying on the dependency graph

[Jeremy Tan]

The most I can prove is smul 1 p ≤ smul (1 / 5) p' from the tile structure definition

[Notification Bot]

13 messages were moved here from #Carleson > Outstanding Tasks, V1 by Jeremy Tan.

[Jeremy Tan]

The number on the left side can only be increased and that on the right can only be decreased, and so I don't know how to conclude smul 1 p ≤ smul 1 p', from which I could conclude Equation (5.3.3) @Edward van de Meent

[Jeremy Tan]

Confirmed that (5.3.3) is false as written:

/-- Lemma 5.3.3, Equation (5.3.3) -/
lemma wiggle_order_11_10 {n : ℝ} (hp : p ≤ p') (hn : 11 / 10 ≤ n) : smul n p ≤ smul n p' := by
  refine ⟨hp.1, ?_⟩
  change ball_{𝓘 p'} (𝒬 p') n ⊆ ball_{𝓘 p} (𝒬 p) n
  rcases eq_or_ne (𝓘 p) (𝓘 p') with h | h
  · rw [h]
    apply ball_subset_ball'
    rw [add_le_iff_nonpos_right]
    have : 0 ≤ dist_{𝓘 p'} (𝒬 p) (𝒬 p') := dist_nonneg
    rcases this.eq_or_lt with k | k
    · rw [k, dist_comm]
    · rw [← not_le] at k
      -- k : ¬dist (𝒬 p) (𝒬 p') ≤ 0
      -- ⊢ dist (𝒬 p') (𝒬 p) ≤ 0
      sorry
  · have : smul 1 p ≤ smul 5⁻¹ p' := ⟨hp.1, (cdist_subset.trans hp.2).trans subset_cdist⟩
    sorry

The hypothesis should be smul 1 p ≤ smul 1 p'

[Jeremy Tan]

@Floris van Doorn :up:

[Floris van Doorn]

Jeremy, I really appreciate your enthusiasm for this project, and the amount of effort you put into this. But please keep in mind the following:

1. if someone else claims a task, don't start doing it yourself. If you want to work on it, and you feel like the other person is not working on it, ask them if you can take over their task, and only start working on it once they reply yes (and don't argue with them if they reply no). I will post more tasks soon, that you can work on if you want.
2. There are other things I'm also working on, so I might not be able to reply to all of your questions within 15 hours. Rest assured that I will reply to them once I have time to work on this project.

[Floris van Doorn]

But you are right, there is a typo in that part of the blueprint. I will fix it.

[Ruben Van de Velde]

Luckily in this case, I hadn't gotten around to working on it again, so no work lost

[Jeremy Tan]

I'm still not convinced that 5.3.3 is true if the cubes are the same (𝓘 p = 𝓘 p'). Consider the following diagram:

[Jeremy Tan]

20240704_222008.jpg

[Jeremy Tan]

which represents the proof context at the sorry of wiggle_order_11_10 at https://github.com/fpvandoorn/carleson/pull/56

[Jeremy Tan]

Intuitively I can "expand" both balls of radius 1 by n - 1 and then I'd have it. However this depends on me being able to find, for an arbitrary point x in the ball of radius n around 𝒬 p', a strictly in-between point s such that the triangle inequality is an equality (dist x s + dist s 𝒬 p = dist x 𝒬 p'). Nothing in the definitions allows me to do that

[Jeremy Tan]

Or am I missing something?

[Jeremy Tan]

/-- Lemma 5.3.3, Equation (5.3.3) -/
lemma wiggle_order_11_10 {n : ℝ} (hp : smul 1 p ≤ smul 1 p') (hn : C5_3_3 a ≤ n) :
    smul n p ≤ smul n p' := by
  rcases eq_or_ne (𝓘 p) (𝓘 p') with h | h
  · refine ⟨hp.1, ?_⟩
    change ball_{𝓘 p'} (𝒬 p') n ⊆ ball_{𝓘 p} (𝒬 p) n
    have y : ball_{𝓘 p'} (𝒬 p') 1 ⊆ ball_{𝓘 p} (𝒬 p) 1 := hp.2
    rw [← h] at y ⊢
    -- y : ball (𝒬 p') 1 ⊆ ball (𝒬 p) 1
    -- ⊢ ball (𝒬 p') n ⊆ ball (𝒬 p) n
    sorry
  · calc
      _ ≤ smul (1 + C2_1_2 a * n) p := by
        apply smul_mono_left
        rwa [← le_sub_iff_add_le, ← one_sub_mul, ← inv_pos_le_iff_one_le_mul']
        linarith [C2_1_2_le_inv_512 (X := X)]
      _ ≤ _ := smul_C2_1_2 n h hp

[Edward van de Meent]

didn't we agree that it is a direct consequence of 5.3.1?

[Jeremy Tan]

No it's not. I start with smul 1 p ≤ smul 1 p' and want smul n p ≤ smul n p' where 1 ≤ n. But I can only decrease the scale factor on the RHS of the inequality with smul_mono, so I cannot get ... ≤ smul n p'

[Edward van de Meent]

aha...

[Jeremy Tan]

I had a little chat with Bhavik about this in the Xena Project server. It seems that proving (5.3.3) for equal cubes depends on assuming the property in the code here -> https://leanprover.zulipchat.com/#narrow/stream/442935-Carleson/topic/Outstanding.20Tasks.2C.20V1/near/446420527

[Jeremy Tan]

which is not true in general

[Floris van Doorn]

Yes, I'm also looking into it now, and I'm coming to the same conclusion. This might be another slip-up where a property of a vector space is assumed that need not hold in this case. I just emailed by co-authors about this, they will know better how to fix this.
Thanks for reporting!

[Floris van Doorn]

In the end, the previous version of the blueprint was correct, when we were still assuming that $q \le q'$.
You cannot apply Lemma 5.3.2 in that case, but you can mimic the proof and still get the correct bound. I finished the formalization of this.

[Floris van Doorn]

I generalized Lemma 5.3.2 a tiny bit so that it can be used to prove 5.3.3 again (this is not yet incorporated in the blueprint).