Rounding errors in the proofs

Stream: Carleson

[Jeremy Tan]

There appear to be errors in many of the proofs related to the status of the central adjustable parameter a as a real and not a natural number. Earlier I saw that in Θ.finite_and_mk_le_of_le_dist the constant C2_1_1 had to be changed from 2 ^ (k * a) to 2 ^ (k * ⌈a⌉₊).

I'm now trying to prove 𝓓.dist_strictMono and I have realised that there is no way to conclude the second inequality in (2.1.1) if a is non-integral:

$$d_{B(c(I), 4 D^{s(I)})}(f, g) \le 2^{-100a} d_{B(c(I), 4D^{s(J)})}(f, g)$$

This is because although you can iterate (1.0.10), you can only do so a whole number of times, so the best inequality I can get is dist_{c I, 4 * D ^ s I} f g ≤ (dist_{c I, 2 ^ (a * 100 * ⌊a⌋₊) * 4 * D ^ s I} f g) / 2 ^ (100 * ⌊a⌋₊). There is no way to deduce the floorless version from this, and the floorless version is required to prove 𝓓.dist_strictMono since 2 ^ (a * 100 * a) = D.

Can we just make a natural and avoid all these little rounding problems?

[Jeremy Tan]

Actually the blueprint says that a is natural, but all the definitions assume a is real!
image.png

[Jeremy Tan]

I make a and A = 2 ^ a natural in https://github.com/fpvandoorn/carleson/pull/48

[Jeremy Tan]

D is natural too but no need to change its type

[Mauricio Collares]

I assume you already have a partial proof of 𝓓.dist_strictMono when a is real, and it got stuck somewhere. If so, can you link to the Lean code for that? I think this might help the maintainers decide which fix is better (there's probably a local fix adding more floors and ceilings).

[Jeremy Tan]

Mauricio Collares said:

I assume you already have a partial proof of 𝓓.dist_strictMono when a is real, and it got stuck somewhere. If so, can you link to the Lean code for that? I think this might help the maintainers decide which fix is better (there's probably a local fix adding more floors and ceilings).

out.diff
Still waiting for Floris or Thiele to merge my pending PRs

[Jeremy Tan]

lemma Grid.dist_strictMono {I J : Grid X} (hpq : I < J) {f g : Θ X} :
    dist_{I} f g ≤ C2_1_2 a * dist_{J} f g := by
  have key := le_cdist_iterate (x := c I) (r := 4 * D ^ s I)
    (by simp only [defaultD]; positivity) f g (100 * ⌊a⌋₊)
  -- key : 2 ^ (100 * ⌊a⌋₊) * dist_{I} f g ≤ dist_{I, A ^ (100 * ⌊a⌋₊) * (4 * D ^ s I)} f g
  rw [← le_div_iff' (by positivity)] at key
  calc
    _ ≤ dist_{c I, 4 * D ^ s I} f g :=
      cdist_mono (ball_subset_ball (by simp_rw [div_eq_inv_mul, defaultD]; gcongr; norm_num))
    _ ≤ 2 ^ (-100 * a) * dist_{c I, 4 * D ^ s J} f g := by
      rw [← div_le_iff' (by positivity), mul_comm _ a, Real.rpow_mul zero_le_two,
        Real.rpow_neg (by positivity), div_inv_eq_mul, mul_comm]
      -- I am supposed to use `key` here, but `key` cannot be manipulated into this step's inequality
      -- becuase of the floors and ceilings
      sorry
    _ ≤ _ := sorry

[Jeremy Tan]

In the meantime I have made more numbers related to a natural in my PR, with adjustments to the proofs as necessary

[Mauricio Collares]

Hmm, C2_1_2 is missing floor signs if I understand correctly.

[Mauricio Collares]

(I'm not informed enough to have an opinion on the relative merits of a being real or natural)

[Floris van Doorn]

Thanks. I'm fine with changing a to be natural, since it is indeed leading to some translation issues. I'm a bit worried about the casts we now have to fiddle with, but we can cast the numbers to reals eagerly, and then it should mostly be fine.
@Jeremy Tan I commented on all your PRs. Thanks for your contributions!

[Edward van de Meent]

i'm going through adapting my proofs to the changes of pull 48 , and as a first comment i'd like to say that it currently seems to be commonly the case that i'd like S to be integer rather than natural, and D to be real. this is because it is common in part 4.1 to do calculations like $D^{-S}$, and feed it to ball and the like...

[Jeremy Tan]

Edward van de Meent said:

i'm going through adapting my proofs to the changes of pull 48 , and as a first comment i'd like to say that it currently seems to be commonly the case that i'd like S to be integer rather than natural, and D to be real. this is because it is common in part 4.1 to do calculations like $D^{-S}$, and feed it to ball and the like...

If you have to do a coercion do it as early as possible

[Edward van de Meent]

as early as possible would be changing the type of D... is that what you mean?

[Jeremy Tan]

defaultD_pos for example should cast the RHS to a real explicitly. There are some exact_mod_casts that were added in #48 that I'll be fixing in my next PR

[Jeremy Tan]

lemma defaultD_pos (a : ℕ) : 0 < (defaultD a : ℝ) := by rw [defaultD]; positivity

[Jeremy Tan]

Even though the scale limit S is unrelated to a I made it a natural because negative S is nonsense for the range [-S, S]

[Edward van de Meent]

how do you mean nonsense? negative S is included in that range?

[Floris van Doorn]

@Edward van de Meent For now, just write D ^ (- (S : \Z)) manually.

[Edward van de Meent]

yes, that's what i'm doing for now... i just wanted to mention it so that if we want to change it later, we know what kind of considerations are to be made

[Yaël Dillies]

D^(-S : \Z) is enough, FWIW

[Floris van Doorn]

I think you're right that it probably makes sense to define S as an integer.

[Jeremy Tan]

Edward van de Meent said:

i'm going through adapting my proofs to the changes of pull 48 , and as a first comment i'd like to say that it currently seems to be commonly the case that i'd like S to be integer rather than natural, and D to be real. this is because it is common in part 4.1 to do calculations like $D^{-S}$, and feed it to ball and the like...

See https://github.com/fpvandoorn/carleson/pull/50

[Jeremy Tan]

Wrap D alone in the cast-to-real, not any larger expression involving it. Same for S or -S in cast-to-integer