chore: adjust the constants in the blueprint to the formalization (#473)

Also optimize a tiny bit one argument, giving very slightly better
constants in the end.

And fix the hyperlinks in the pdf file of the blueprint.

Author: sgouezel

Carleson/Antichain/AntichainOperator.lean

@@ -231,7 +231,8 @@ lemma M14_bound (hg : MemLp g 2 volume) :
   rw [show (2 : ℝ≥0∞) = (2 : ℝ≥0) by rfl, ← ENNReal.coe_pow, ENNReal.coe_le_coe]
   exact C2_0_6_q₆_le a4
 
-/-- Constant appearing in Lemma 6.1.4. -/
+/-- Constant appearing in Lemma 6.1.4.
+Has value `2 ^ (117 * a ^ 3)` in the blueprint. -/
 irreducible_def C6_1_4 (a : ℕ) : ℝ≥0 := 2 ^ ((𝕔 + 5 + 𝕔 / 8) * a ^ 3)
 
 lemma le_C6_1_4 (a4 : 4 ≤ a) :
@@ -314,30 +315,30 @@ lemma dens1_antichain (h𝔄 : IsAntichain (· ≤ ·) 𝔄) (hf : Measurable f)
       grw [← ENNReal.rpow_le_rpow_iff (show (0 : ℝ) < (2 : ℕ) by norm_num),
         ENNReal.rpow_natCast, ENNReal.rpow_natCast, dens1_antichain_sq h𝔄 hg hgG]
 
-/-- The constant appearing in Proposition 2.0.3. -/
-def C2_0_3 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := 2 ^ ((𝕔 + 8 + 𝕔 / 8) * a ^ 3) / (q - 1)
+/-- The constant appearing in Proposition 2.0.3.
+Has value `2 ^ (117 * a ^ 3)` in the blueprint. -/
+def C2_0_3 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := 2 ^ ((𝕔 + 5 + 𝕔 / 8) * a ^ 3) / (q - 1)
 
 variable (X) in
 omit [TileStructure Q D κ S o] in
 private lemma ineq_aux_2_0_3 :
     ((2 ^ ((𝕔 + 5 + 𝕔 / 8 : ℕ) * a ^ 3) : ℝ≥0) : ℝ≥0∞) ^ (q - 1) *
-      (((2 ^ ((𝕔 + 8) * a ^ 3) : ℝ≥0) : ℝ≥0∞) * (nnq - 1)⁻¹) ^ (2 - q) ≤
-        (2 ^ ((𝕔 + 8 + 𝕔 / 8 : ℕ) * a ^ 3) / (nnq - 1) : ℝ≥0) := by
+    (((2 ^ ((𝕔 + 3) * a ^ 3) : ℝ≥0) : ℝ≥0∞) * (nnq - 1)⁻¹) ^ (2 - q) ≤
+    (2 ^ ((𝕔 + 5 + 𝕔 / 8 : ℕ) * a ^ 3) / (nnq - 1) : ℝ≥0) := by
   have hq1 : 0 ≤ q - 1 := sub_nonneg.mpr (NNReal.coe_le_coe.mpr (nnq_mem_Ioc X).1.le)
   have hq2 : 0 ≤ 2 - q := sub_nonneg.mpr (NNReal.coe_le_coe.mpr (nnq_mem_Ioc X).2)
   have h21 : (2 : ℝ) - 1 = 1 := by norm_num
   calc
     _ = ((2 ^ ((𝕔 + 5 + 𝕔 / 8 : ℕ) * a ^ 3) : ℝ≥0) : ℝ≥0∞) ^ (q - 1) *
-        (((2 ^ ((𝕔 + 8 + 0) * a ^ 3) : ℝ≥0) : ℝ≥0∞)) ^ (2 - q) * (nnq - 1)⁻¹ ^ (2 - q) := by
+        (((2 ^ ((𝕔 + 3 + 0) * a ^ 3) : ℝ≥0) : ℝ≥0∞)) ^ (2 - q) * (nnq - 1)⁻¹ ^ (2 - q) := by
       rw [ENNReal.mul_rpow_of_nonneg _ _ hq2]; ring
-    _ ≤ ((2 ^ ((𝕔 + 8 + 𝕔 / 8 : ℕ) * a ^ 3) : ℝ≥0) : ℝ≥0∞) ^ (q - 1) *
-        (((2 ^ ((𝕔 + 8 + 𝕔 / 8 : ℕ) * a ^ 3) : ℝ≥0) : ℝ≥0∞)) ^ (2 - q) * (nnq - 1)⁻¹ := by
+    _ ≤ ((2 ^ ((𝕔 + 5 + 𝕔 / 8 : ℕ) * a ^ 3) : ℝ≥0) : ℝ≥0∞) ^ (q - 1) *
+        (((2 ^ ((𝕔 + 5 + 𝕔 / 8 : ℕ) * a ^ 3) : ℝ≥0) : ℝ≥0∞)) ^ (2 - q) * (nnq - 1)⁻¹ := by
       have h11 : (1 + 1 : ℝ≥0) = 2 := by norm_num
       gcongr
       · norm_num
       · norm_num
       · norm_num
-      · simp
       · refine ENNReal.rpow_le_self_of_one_le ?_ (by linarith)
         rw [one_le_coe_iff, one_le_inv₀ (tsub_pos_iff_lt.mpr (nnq_mem_Ioc X).1), tsub_le_iff_right,
           h11]; exact (nnq_mem_Ioc X).2
@@ -369,8 +370,7 @@ theorem antichain_operator (h𝔄 : IsAntichain (· ≤ ·) 𝔄) (hf : Measurab
     simp only [hq2, h21, one_div, sub_self, ENNReal.rpow_zero, mul_one]
     apply (dens1_antichain h𝔄 hf hf1 hg hg1).trans
     gcongr
-    simp only [C2_0_3, hnnq2, h21', div_one, C6_1_4]
-    gcongr <;> norm_num
+    simp only [C6_1_4, C2_0_3, hnnq2, h21', div_one, le_refl]
   · have hq2' : 0 < 2 - q :=
       sub_pos.mpr (lt_of_le_of_ne (NNReal.coe_le_coe.mpr (nnq_mem_Ioc X).2) hq2)
     -- Take the (2-q)-th power of 6.1.11

Carleson/Antichain/Basic.lean

@@ -87,8 +87,9 @@ lemma tile_disjointness {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ ·) (
 
 open ENNReal Metric NNReal Real
 
-/-- Constant appearing in Lemma 6.1.2. -/
-noncomputable def C6_1_2 (a : ℕ) : ℕ := 2 ^ ((𝕔 + 7) * a ^ 3)
+/-- Constant appearing in Lemma 6.1.2.
+Has value `2 ^ (102 * a ^ 3)` in the blueprint. -/
+noncomputable def C6_1_2 (a : ℕ) : ℕ := 2 ^ ((𝕔 + 2) * a ^ 3)
 
 lemma C6_1_2_ne_zero (a : ℕ) : (C6_1_2 a : ℝ≥0∞) ≠ 0 := by rw [C6_1_2]; positivity
 
@@ -212,13 +213,9 @@ lemma maximal_bound_antichain {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤
       · gcongr
         rw [C6_1_2, add_comm (5 * a), add_assoc]; norm_cast
         apply pow_le_pow_right₀ one_le_two
-        calc
-        _ ≤ (𝕔 + 1) * a ^ 3  + 6 * a ^ 3:= by
-          rw [add_le_add_iff_left]
-          ring_nf
-          gcongr
-          exact le_self_pow₀ (by linarith [four_le_a X]) (by omega)
-        _ = (𝕔 + 7) * a ^ 3 := by ring
+        ring_nf
+        suffices 6 * a ≤ a ^ 3 by omega
+        linarith [sixteen_times_le_cube (four_le_a X)]
       · exact lt_of_le_of_lt hdist_cp
           (mul_lt_mul_of_nonneg_of_pos (by linarith) (le_refl _) (by linarith) hDpow_pos)
     _ ≤ C6_1_2 a * MB volume 𝔄 𝔠 (8 * D ^ 𝔰 ·) f x := by
@@ -232,8 +229,8 @@ lemma maximal_bound_antichain {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤
     simp [h0]
 
 /-- Constant appearing in Lemma 6.1.3.
-Note: the proof shows that `111` can be replaced by `108`. -/
-noncomputable def C6_1_3 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := 2 ^ ((𝕔 + 8) * a ^ 3) * (q - 1)⁻¹
+Has value `2 ^ (103 * a ^ 3)` in the blueprint. -/
+noncomputable def C6_1_3 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := 2 ^ ((𝕔 + 3) * a ^ 3) * (q - 1)⁻¹
 
 -- Namespace for auxiliaries used in the proof of Lemma 6.1.3.
 namespace Lemma6_1_3
@@ -411,8 +408,8 @@ lemma const_check : C6_1_2 a * C2_0_6 (defaultA a) (p X).toNNReal 2 ≤ C6_1_3 a
           _ = (2 * q - 1) * (q - 1)⁻¹ := by field_simp [hqiq]
           _ ≤ _ := by gcongr; linarith only [q_mem_Ioc X |>.2]
   calc
-    _ ≤ 2 ^ ((𝕔 + 7) * a ^ 3) * (2 ^ (2 * a + 4) * (q - 1)⁻¹) := by simp [C6_1_2, hc_le]
-    _ ≤ 2 ^ ((𝕔 + 8) * a ^ 3) * (q - 1)⁻¹ := by
+    _ ≤ 2 ^ ((𝕔 + 2) * a ^ 3) * (2 ^ (2 * a + 4) * (q - 1)⁻¹) := by simp [C6_1_2, hc_le]
+    _ ≤ 2 ^ ((𝕔 + 3) * a ^ 3) * (q - 1)⁻¹ := by
       rw [← mul_assoc, ← pow_add]
       gcongr
       · norm_num