feat: complete proof of Lemma 8.0.1 (#278)

I've also made a few changes throughout the files to get the right
statement of Lemma 8.0.1:
* instead of the norms `iLipNorm` (Lipschitz) and `hnorm` (Hölder), we
now have versions defined using sups in ENNReal, called `iLipENorm` and
`iHolENorm`, and their images in NNReal called `iLipNNNorm` and
`iHolNNNorm`.
* The definition of the Hölder norm has been fixed. It used to be
```lean
⨆ (x ∈ ball x₀ R), (‖ϕ x‖₊ : ℝ≥0∞) +
  R ^ τ * ⨆ (x ∈ ball x₀ R) (y ∈ ball x₀ R) (_ : x ≠ y), (‖ϕ x - ϕ y‖₊ / (nndist x y) ^ τ : ℝ≥0∞)
```
where the second sup was included in the first sup because of the lack
of parentheses.
* The definition of the class `IsCancellative` has been fixed: it
required the test function to be globally Lipschitz, while the right
condition is Lipschitz on a ball
* With the change of `IsCancellative`, the proof that it is satisfied on
the real line becomes harder. I had to change a little bit the Lean
statement and proof of the classical Van der Corput lemma (requiring
only a Lipschitz function on a ball) -- now it matches the statement in
the blueprint.
* I have streamlined the proof of `IsCancellative` on the real line,
using new API around the Lipschitz and Hölder norms
* For doubling measures, I have added the statement
```lean
lemma measure_ball_le_same'' (x : X) {r t : ℝ} (ht : 0 < t) (h't : t ≤ 1) :
    μ.real (ball x r) ≤ A * t ^ (- Real.logb 2 A) * μ.real (ball x (t * r))
```
Once this is established, this avoids juggling with powers of 2 in the
proof of Lemma 8.0.1. I don't know if there are other places in the
files where it could be used to streamline arguments.
* Use enorm instead of the coercion of nnnorm wherever I've noticed it

I can split in in smaller PRs if you prefer.

---------

Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

Author: sgouezel

Carleson/Antichain/TileCorrelation.lean

@@ -38,58 +38,67 @@ lemma ENNReal.mul_div_mul_comm {a b c d : ℝ≥0∞} (hc : c ≠ ⊤) (hd : d 
   ring
 
 lemma aux_6_2_3 (s₁ s₂ : ℤ) (x₁ x₂ y y' : X)  :
-  (‖Ks s₂ x₂ y‖₊ : ℝ≥0∞) * (‖Ks s₁ x₁ y - Ks s₁ x₁ y'‖₊ : ℝ≥0∞) ≤
+  ‖Ks s₂ x₂ y‖ₑ * ‖Ks s₁ x₁ y - Ks s₁ x₁ y'‖ₑ ≤
   ↑(C2_1_3 ↑a) / volume (ball x₂ (↑D ^ s₂)) *
     (↑(D2_1_3 ↑a) / volume (ball x₁ (↑D ^ s₁)) * (↑(nndist y y') ^ τ / ↑((D : ℝ≥0) ^ s₁) ^ τ)) := by
   have hτ : 0 ≤ τ := by simp only [defaultτ, inv_nonneg, Nat.cast_nonneg]
-  apply mul_le_mul nnnorm_Ks_le _ (zero_le _) (zero_le _)
+  apply mul_le_mul enorm_Ks_le _ (zero_le _) (zero_le _)
   convert nnnorm_Ks_sub_Ks_le
   rw [← ENNReal.div_rpow_of_nonneg _ _ hτ]
   simp only [defaultτ]
   congr
   rw [ENNReal.coe_zpow (by simp)]
   rfl
 
+/- TODO: PR-/
+@[simp, rclike_simps] lemma _root_.RCLike.enorm_conj {𝕜 : Type*} [RCLike 𝕜] (z : 𝕜) :
+    ‖conj z‖ₑ = ‖z‖ₑ := by simp [enorm]
+
+namespace Real
+
+/- TODO: PR-/
+theorem toNNReal_zpow {x : ℝ} (hx : 0 ≤ x) (n : ℤ) : (x ^ n).toNNReal = x.toNNReal ^ n := by
+  rw [← NNReal.coe_inj, NNReal.coe_zpow, Real.coe_toNNReal _ (zpow_nonneg hx _),
+    Real.coe_toNNReal x hx]
+
+end Real
+
 -- Eq. 6.2.3 (Lemma 6.2.1)
 lemma correlation_kernel_bound (ha : 1 < a) {s₁ s₂ : ℤ} (hs₁ : s₁ ∈ Icc (- (S : ℤ)) s₂)
    {x₁ x₂ : X} :
-    hnorm (a := a) (correlation s₁ s₂ x₁ x₂) x₁ (↑D ^s₁) ≤
+    iHolENorm (correlation s₁ s₂ x₁ x₂) x₁ (↑D ^s₁) ≤
       (C_6_2_1 a : ℝ≥0∞) / (volume (ball x₁ (↑D ^s₁)) * volume (ball x₂ (↑D ^s₂))) := by
   -- 6.2.4
-  have hφ' : ∀ y : X, ‖correlation s₁ s₂ x₁ x₂ y‖₊ ≤
+  have hφ' (y : X) : ‖correlation s₁ s₂ x₁ x₂ y‖ₑ ≤
       (C2_1_3 a)^2 / ((volume (ball x₁ (D ^ s₁))) * (volume (ball x₂ (D ^ s₂)))) := by
-    intro y
-    simp only [correlation, nnnorm_mul, RCLike.nnnorm_conj, ENNReal.coe_mul, pow_two,
+    simp only [correlation, enorm_mul, RCLike.enorm_conj, pow_two,
       ENNReal.mul_div_mul_comm (measure_ball_ne_top _ _) (measure_ball_ne_top _ _)]
-    exact mul_le_mul nnnorm_Ks_le nnnorm_Ks_le (zero_le _) (zero_le _)
-
+    exact mul_le_mul enorm_Ks_le enorm_Ks_le (zero_le _) (zero_le _)
   -- 6.2.6 + 6.2.7
-  have hsimp :  ∀ (y y' : X),
-      (‖correlation s₁ s₂ x₁ x₂ y - correlation s₁ s₂ x₁ x₂ y'‖₊ : ℝ≥0∞) ≤
-        ‖Ks s₁ x₁ y - Ks s₁ x₁ y'‖₊ * ‖Ks s₂ x₂ y‖₊ +
-          ‖Ks s₁ x₁ y'‖₊ * ‖Ks s₂ x₂ y - Ks s₂ x₂ y'‖₊ := by
+  have hsimp : ∀ (y y' : X),
+      ‖correlation s₁ s₂ x₁ x₂ y - correlation s₁ s₂ x₁ x₂ y'‖ₑ ≤
+        ‖Ks s₁ x₁ y - Ks s₁ x₁ y'‖₊ * ‖Ks s₂ x₂ y‖ₑ +
+          ‖Ks s₁ x₁ y'‖₊ * ‖Ks s₂ x₂ y - Ks s₂ x₂ y'‖ₑ := by
     intro y y'
-    calc (‖correlation s₁ s₂ x₁ x₂ y - correlation s₁ s₂ x₁ x₂ y'‖₊ : ℝ≥0∞)
+    calc ‖correlation s₁ s₂ x₁ x₂ y - correlation s₁ s₂ x₁ x₂ y'‖ₑ
       _ = ‖conj (Ks s₁ x₁ y) * Ks s₂ x₂ y - conj (Ks s₁ x₁ y') * Ks s₂ x₂ y +
-          (conj (Ks s₁ x₁ y') * Ks s₂ x₂ y - conj (Ks s₁ x₁ y') * (Ks s₂ x₂ y'))‖₊ := by
+          (conj (Ks s₁ x₁ y') * Ks s₂ x₂ y - conj (Ks s₁ x₁ y') * (Ks s₂ x₂ y'))‖ₑ := by
         simp only [correlation, sub_add_sub_cancel]
-      _ ≤ ‖conj (Ks s₁ x₁ y) * Ks s₂ x₂ y - conj (Ks s₁ x₁ y') * Ks s₂ x₂ y ‖₊ +
-          ‖conj (Ks s₁ x₁ y') * Ks s₂ x₂ y - conj (Ks s₁ x₁ y') * (Ks s₂ x₂ y')‖₊ := by
-            norm_cast
-            exact nnnorm_add_le _ _
-      _ = ‖Ks s₁ x₁ y - Ks s₁ x₁ y'‖₊ * ‖Ks s₂ x₂ y‖₊ +
-          ‖Ks s₁ x₁ y'‖₊ * ‖Ks s₂ x₂ y - Ks s₂ x₂ y'‖₊ := by
-          norm_cast
-          simp only [← sub_mul, ← mul_sub, nnnorm_mul, RCLike.nnnorm_conj, ← map_sub]
+      _ ≤ ‖conj (Ks s₁ x₁ y) * Ks s₂ x₂ y - conj (Ks s₁ x₁ y') * Ks s₂ x₂ y ‖ₑ +
+          ‖conj (Ks s₁ x₁ y') * Ks s₂ x₂ y - conj (Ks s₁ x₁ y') * (Ks s₂ x₂ y')‖ₑ :=
+            enorm_add_le _ _
+      _ = ‖Ks s₁ x₁ y - Ks s₁ x₁ y'‖ₑ * ‖Ks s₂ x₂ y‖ₑ +
+          ‖Ks s₁ x₁ y'‖ₑ * ‖Ks s₂ x₂ y - Ks s₂ x₂ y'‖ₑ := by
+          simp only [← sub_mul, ← mul_sub, enorm_mul, RCLike.enorm_conj, ← map_sub]
   -- 6.2.5
   have hyy' : ∀ (y y' : X) (hy' : y ≠ y'), (((D  ^ s₁ : ℝ≥0)) ^ τ)  *
-    (‖correlation s₁ s₂ x₁ x₂ y - correlation s₁ s₂ x₁ x₂ y'‖₊ / (nndist y y')^τ) ≤
+    (‖correlation s₁ s₂ x₁ x₂ y - correlation s₁ s₂ x₁ x₂ y'‖ₑ / (nndist y y')^τ) ≤
       (2^(253*a^3) / (volume (ball x₁ (↑D ^s₁)) * volume (ball x₂ (↑D ^s₂)))) := by
     intros y y' hy'
     rw [mul_comm, ← ENNReal.le_div_iff_mul_le, ENNReal.div_le_iff_le_mul]
-    calc (‖correlation s₁ s₂ x₁ x₂ y - correlation s₁ s₂ x₁ x₂ y'‖₊ : ℝ≥0∞)
-      _ ≤ ‖Ks s₁ x₁ y - Ks s₁ x₁ y'‖₊ * ‖Ks s₂ x₂ y‖₊ +
-          ‖Ks s₁ x₁ y'‖₊ * ‖Ks s₂ x₂ y - Ks s₂ x₂ y'‖₊ := hsimp y y' -- 6.2.6 + 6.2.7
+    calc ‖correlation s₁ s₂ x₁ x₂ y - correlation s₁ s₂ x₁ x₂ y'‖ₑ
+      _ ≤ ‖Ks s₁ x₁ y - Ks s₁ x₁ y'‖ₑ * ‖Ks s₂ x₂ y‖ₑ +
+          ‖Ks s₁ x₁ y'‖ₑ * ‖Ks s₂ x₂ y - Ks s₂ x₂ y'‖ₑ := hsimp y y' -- 6.2.6 + 6.2.7
       _ ≤ 2 ^ (252 * a ^ 3) / (volume (ball x₁ (↑D ^ s₁)) * volume (ball x₂ (↑D ^ s₂))) *
         (↑(nndist y y') ^ τ / ((D ^ s₁ : ℝ≥0) : ℝ≥0∞) ^ τ +
           ↑(nndist y y') ^ τ / ((D ^ s₂ : ℝ≥0) : ℝ≥0∞) ^ τ) := by
@@ -101,7 +110,7 @@ lemma correlation_kernel_bound (ha : 1 < a) {s₁ s₂ : ℤ} (hs₁ : s₁ ∈
         simp only [ENNReal.mul_div_mul_comm (measure_ball_ne_top _ _) (measure_ball_ne_top _ _),
           mul_assoc]
         apply add_le_add (aux_6_2_3 s₁ s₂ x₁ x₂ y y')
-        rw [← neg_sub, nnnorm_neg]
+        rw [← neg_sub, enorm_neg]
         convert aux_6_2_3 s₂ s₁ x₂ x₁ y' y using 1
         simp only [← mul_assoc, ← ENNReal.mul_div_mul_comm (measure_ball_ne_top _ _)
           (measure_ball_ne_top _ _)]
@@ -175,15 +184,17 @@ lemma correlation_kernel_bound (ha : 1 < a) {s₁ s₂ : ℤ} (hs₁ : s₁ ∈
     · left
       refine ENNReal.rpow_ne_top_of_nonneg ?ht.h.hy0 ENNReal.coe_ne_top
       simp only [defaultτ, inv_nonneg, Nat.cast_nonneg]
-  calc hnorm (a := a) (correlation s₁ s₂ x₁ x₂) x₁ (↑D ^s₁)
+  calc iHolENorm (correlation s₁ s₂ x₁ x₂) x₁ (↑D ^s₁)
     _ ≤ (C2_1_3 a)^2 / ((volume (ball x₁ (D ^ s₁))) * (volume (ball x₂ (D ^ s₂)))) +
         (2^(253*a^3) / (volume (ball x₁ (↑D ^s₁)) * volume (ball x₂ (↑D ^s₂)))) := by
-        simp only [hnorm]
-        refine iSup₂_le ?h
-        intro y _
-        apply add_le_add (hφ' y)
+        simp only [iHolENorm]
+        apply add_le_add
+        · simp only [iSup_le_iff, hφ', implies_true]
         simp only [ENNReal.mul_iSup, iSup_le_iff]
-        exact fun z _ z' _ hzz' ↦ hyy' z z' hzz'
+        intro z hz z' hz' hzz'
+        convert hyy' z z' hzz'
+        · rw [ENNReal.ofReal, Real.toNNReal_zpow D_nonneg, Real.toNNReal_coe_nat]
+        · exact edist_nndist z z'
     _ ≤ (C_6_2_1 a : ℝ≥0∞) / (volume (ball x₁ (↑D ^s₁)) * volume (ball x₂ (↑D ^s₂))) := by
       have h12 : (1 : ℝ≥0∞) ≤ 2 := one_le_two
       have h204 : 204 ≤ 253 := by omega

Carleson/Classical/CarlesonOnTheRealLine.lean

@@ -388,26 +388,19 @@ instance compatibleFunctions_R : CompatibleFunctions ℝ ℝ (2 ^ 4) where
     intro x R R' f
     exact integer_ball_cover.mono_nat (by norm_num)
 
+open scoped NNReal
 
 instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
   /- Lemma 11.7.12 (real van der Corput) from the paper. -/
   norm_integral_exp_le := by
-    intro x r ϕ K hK _ f g
-    by_cases r_pos : 0 ≥ r
-    · rw [ball_eq_empty.mpr r_pos]
+    intro x r ϕ hK _ f g
+    rcases le_or_lt r 0 with r_nonpos | r_pos
+    · rw [ball_eq_empty.mpr r_nonpos]
       simp
-    push_neg at r_pos
     rw [defaultτ, ← one_div, measureReal_def, Real.volume_ball,
       ENNReal.toReal_ofReal (by linarith [r_pos]), Real.ball_eq_Ioo, ← integral_Ioc_eq_integral_Ioo,
       ← intervalIntegral.integral_of_le (by linarith [r_pos]), dist_integer_linear_eq,
       max_eq_left r_pos.le]
-    set L : NNReal :=
-      ⟨⨆ (x : ℝ) (y : ℝ) (_ : x ≠ y), ‖ϕ x - ϕ y‖ / dist x y,
-        Real.iSup_nonneg fun x ↦ Real.iSup_nonneg fun y ↦ Real.iSup_nonneg
-        fun _ ↦ div_nonneg (norm_nonneg _) dist_nonneg⟩ with Ldef
-    set B : NNReal :=
-      ⟨⨆ y ∈ ball x r, ‖ϕ y‖, Real.iSup_nonneg fun i ↦ Real.iSup_nonneg
-        fun _ ↦ norm_nonneg _⟩  with Bdef
     calc ‖∫ (x : ℝ) in x - r..x + r, (Complex.I * (↑(f x) - ↑(g x))).exp * ϕ x‖
       _ = ‖∫ (x : ℝ) in x - r..x + r, (Complex.I * ((↑f - ↑g) : ℤ) * x).exp * ϕ x‖ := by
         congr with x
@@ -416,69 +409,29 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
         push_cast
         rw [_root_.sub_mul]
         norm_cast
-      _ ≤ 2 * π * ((x + r) - (x - r)) * (B + L * ((x + r) - (x - r)) / 2) *
+      _ ≤ 2 * π * ((x + r) - (x - r)) * (iLipNNNorm ϕ x r +
+           (iLipNNNorm ϕ x r / r.toNNReal : ℝ≥0) * ((x + r) - (x - r)) / 2) *
         (1 + |((↑f - ↑g) : ℤ)| * ((x + r) - (x - r)))⁻¹ := by
         apply van_der_Corput (by linarith)
-        · rw [lipschitzWith_iff_dist_le_mul]
-          intro x y
-          --TODO: The following could be externalised as a lemma.
-          by_cases hxy : x = y
-          · rw [hxy]
-            simp
-          rw [dist_eq_norm, ← div_le_iff₀ (dist_pos.mpr hxy), Ldef, NNReal.coe_mk]
-          apply le_ciSup_of_le _ x
-          on_goal 1 => apply le_ciSup_of_le _ y
-          on_goal 1 => apply le_ciSup_of_le _ hxy
-          · rfl
-          · use K
-            rw [upperBounds]
-            simp only [ne_eq, Set.mem_range, exists_prop, and_imp,
-              forall_apply_eq_imp_iff, Set.mem_setOf_eq]
-            intro h
-            rw [div_le_iff₀ (dist_pos.mpr h), dist_eq_norm]
-            exact LipschitzWith.norm_sub_le hK _ _
-          · use K
-            rw [upperBounds]
-            simp only [ne_eq, Set.mem_range, forall_exists_index,
-              forall_apply_eq_imp_iff, Set.mem_setOf_eq]
-            intro y
-            apply Real.iSup_le _ NNReal.zero_le_coe
-            intro h
-            rw [div_le_iff₀ (dist_pos.mpr h), dist_eq_norm]
-            exact LipschitzWith.norm_sub_le hK _ _
-          · use K
-            rw [upperBounds]
-            simp only [ne_eq, Set.mem_range, forall_exists_index,
-              forall_apply_eq_imp_iff, Set.mem_setOf_eq]
-            intro x
-            apply Real.iSup_le _ NNReal.zero_le_coe
-            intro y
-            apply Real.iSup_le _ NNReal.zero_le_coe
-            intro h
-            rw [div_le_iff₀ (dist_pos.mpr h), dist_eq_norm]
-            apply LipschitzWith.norm_sub_le hK
-        · --prove main property of B
-          intro y hy
-          apply ConditionallyCompleteLattice.le_biSup
-          · --TODO: externalize as lemma LipschitzWithOn.BddAbove or something like that?
-            rw [Real.ball_eq_Ioo]
-            exact BddAbove.mono (Set.image_mono Set.Ioo_subset_Icc_self)
-              (isCompact_Icc.bddAbove_image (continuous_norm.comp hK.continuous).continuousOn)
-          use y
-          rw [Real.ball_eq_Ioo]
-          use hy
-      _ = 2 * π * (2 * r) * (B + r * L) * (1 + 2 * r * |((↑f - ↑g) : ℤ)|)⁻¹ := by
+        · rw [Ioo_eq_ball]
+          simp only [sub_add_add_cancel, add_self_div_two, add_sub_sub_cancel]
+          apply LipschitzOnWith.of_iLipENorm_ne_top hK
+        · intro y hy
+          apply norm_le_iLipNNNorm_of_mem hK
+          rwa [Real.ball_eq_Ioo]
+      _ = 2 * π * (2 * r) * (iLipNNNorm ϕ x r + r * (iLipNNNorm ϕ x r / r.toNNReal : ℝ≥0))
+            * (1 + 2 * r * |((↑f - ↑g) : ℤ)|)⁻¹ := by
         ring
-      _ ≤ (2 ^ 4 : ℕ) * (2 * r) * iLipNorm ϕ x r *
+      _ = 2 * π * (2 * r) * (iLipNNNorm ϕ x r + iLipNNNorm ϕ x r)
+            * (1 + 2 * r * |((↑f - ↑g) : ℤ)|)⁻¹ := by
+        congr
+        rw [NNReal.coe_div, Real.coe_toNNReal _ r_pos.le, mul_div_cancel₀ _ r_pos.ne']
+      _ = 4 * π * (2 * r) * iLipNNNorm ϕ x r * (1 + 2 * r * ↑|(↑f - ↑g : ℤ)|)⁻¹ := by ring
+      _ ≤ (2 ^ 4 : ℕ) * (2 * r) * iLipNNNorm ϕ x r *
         (1 + 2 * r * ↑|(↑f - ↑g : ℤ)|) ^ (- (1 / (4 : ℝ))) := by
         gcongr
-        · exact mul_nonneg (mul_nonneg (by norm_num) (by linarith)) (iLipNorm_nonneg r_pos.le)
         · norm_num
           linarith [pi_le_four]
-        · unfold iLipNorm
-          gcongr
-          · apply le_of_eq Bdef
-          · apply le_of_eq Ldef
         · rw [← Real.rpow_neg_one]
           apply Real.rpow_le_rpow_of_exponent_le _ (by norm_num)
           simp only [Int.cast_abs, Int.cast_sub, le_add_iff_nonneg_right]