From fb4d8261d0ac45726477b23c0e38c26b53a3de5c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mar=C3=ADa=20In=C3=A9s=20de=20Frutos-Fern=C3=A1ndez?= <88536493+mariainesdff@users.noreply.github.com> Date: Thu, 28 Nov 2024 15:13:31 +0100 Subject: [PATCH] Prove lemma 6.3.1 (#190) --- Carleson/Antichain/AntichainTileCount.lean | 107 ++++++++++++++++++++- blueprint/src/chapter/main.tex | 5 +- 2 files changed, 106 insertions(+), 6 deletions(-) diff --git a/Carleson/Antichain/AntichainTileCount.lean b/Carleson/Antichain/AntichainTileCount.lean index 1a24d27b..66ed9058 100644 --- a/Carleson/Antichain/AntichainTileCount.lean +++ b/Carleson/Antichain/AntichainTileCount.lean @@ -2,11 +2,13 @@ import Carleson.TileStructure import Carleson.HardyLittlewood import Carleson.Psi +macro_rules | `(tactic |gcongr_discharger) => `(tactic | with_reducible assumption) + noncomputable section open scoped ENNReal NNReal ShortVariables -open MeasureTheory Set +open MeasureTheory Metric Set namespace Antichain @@ -14,9 +16,106 @@ variable {X : Type*} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q D κ S o] -- Lemma 6.3.1 -lemma tile_reach {ϑ : Θ X} {N : ℕ} {p p' : 𝔓 X} (hp : dist_(p) (𝒬 p) ϑ ≤ 2^N) - (hp' : dist_(p') (𝒬 p') ϑ ≤ 2^N) (hI : 𝓘 p ≤ 𝓘 p') (hs : 𝔰 p < 𝔰 p'): - smul (2^(N + 2)) p ≤ smul (2^(N + 2)) p' := sorry +-- hp is eq. 6.3.1, hp' is eq. 6.3.2. +lemma tile_reach (ha : 4 ≤ a) {ϑ : Θ X} {N : ℕ} {p p' : 𝔓 X} (hp : dist_(p) (𝒬 p) ϑ ≤ 2^N) + (hp' : dist_(p') (𝒬 p') ϑ ≤ 2^N) (hI : 𝓘 p ≤ 𝓘 p') (hs : 𝔰 p < 𝔰 p') : + smul (2^(N + 2)) p ≤ smul (2^(N + 2)) p' := by + -- 6.3.4 + have hp2 : dist_(p) ϑ (𝒬 p') ≤ 2^N := by + rw [dist_comm] + exact le_trans (Grid.dist_mono hI) hp' + -- 6.3.5 + have hp'2 : dist_(p) (𝒬 p) (𝒬 p') ≤ 2^(N + 1) := + calc dist_(p) (𝒬 p) (𝒬 p') + _ ≤ dist_(p) (𝒬 p) ϑ + dist_(p) ϑ (𝒬 p') := dist_triangle _ _ _ + _ ≤ 2^N + 2^N := add_le_add hp hp2 + _ = 2^(N + 1) := by ring + -- Start proof of 6.3.3. + simp only [TileLike.le_def, smul_fst, smul_snd] + refine ⟨hI, fun o' ho' ↦ ?_⟩ -- o' is ϑ' in blueprint, ho' is 6.3.6. + -- 6.3.7 + have hlt : dist_{𝔠 p', 8 * D^𝔰 p'} (𝒬 p') o' < 2^(5*a + N + 2) := by + have hle : dist_{𝔠 p', 8 * D^𝔰 p'} (𝒬 p') o' ≤ (defaultA a) ^ 5 * dist_(p') (𝒬 p') o' := by + have hpos : (0 : ℝ) < D^𝔰 p'/4 := by + rw [div_eq_mul_one_div, mul_comm] + apply mul_defaultD_pow_pos _ (by linarith) + have h8 : (8 : ℝ) * D^𝔰 p' = 2^5 * (D^𝔰 p'/4) := by ring + rw [h8] + exact cdist_le_iterate hpos (𝒬 p') o' 5 + apply lt_of_le_of_lt hle + simp only [defaultA, add_assoc] + rw [pow_add, Nat.cast_pow, Nat.cast_ofNat, ← pow_mul, mul_comm a, dist_comm] + gcongr + exact ho' + -- 6.3.8 + have hin : 𝔠 p ∈ ball (𝔠 p') (4 * D^𝔰 p') := Grid_subset_ball (hI.1 Grid.c_mem_Grid) + -- 6.3.9 + have hball_le : ball (𝔠 p) (4 * D^𝔰 p') ⊆ ball (𝔠 p') (8 * D^𝔰 p') := by + intro x hx + rw [mem_ball] at hx hin ⊢ + calc dist x (𝔠 p') + _ ≤ dist x (𝔠 p) + dist (𝔠 p) (𝔠 p') := dist_triangle _ _ _ + _ < 4 * ↑D ^ 𝔰 p' + 4 * ↑D ^ 𝔰 p' := add_lt_add hx hin + _ = 8 * ↑D ^ 𝔰 p' := by ring + -- 6.3.10 + have hlt2 : dist_{𝔠 p, 4 * D^𝔰 p'} (𝒬 p') o' < 2^(5*a + N + 2) := + lt_of_le_of_lt (cdist_mono hball_le) hlt + -- 6.3.11 + have hlt3 : dist_{𝔠 p, 2^((2 : ℤ) - 5*a^2 - 2*a) * D^𝔰 p'} (𝒬 p') o' < 2^N := by + have hle : 2 ^ ((5 : ℤ)*a + 2) * dist_{𝔠 p, 2^((2 : ℤ) - 5*a^2 - 2*a) * D^𝔰 p'} (𝒬 p') o' ≤ + dist_{𝔠 p, 4 * D^𝔰 p'} (𝒬 p') o' := by + have heq : (defaultA a : ℝ) ^ ((5 : ℤ)*a + 2) * 2^((2 : ℤ) - 5*a^2 - 2*a) = 4 := by + simp only [defaultA, Nat.cast_pow, Nat.cast_ofNat, ← zpow_natCast, ← zpow_mul] + rw [← zpow_add₀ two_ne_zero] + ring_nf + rw [← heq, mul_assoc] + exact le_cdist_iterate (by positivity) (𝒬 p') o' (5*a + 2) + rw [← le_div_iff₀' (by positivity), div_eq_mul_inv, ← zpow_neg, neg_add, ← neg_mul, + ← sub_eq_add_neg, mul_comm _ ((2 : ℝ) ^ _)] at hle + calc dist_{𝔠 p, 2^((2 : ℤ) - 5*a^2 - 2*a) * D^𝔰 p'} (𝒬 p') o' + _ ≤ 2^(-(5 : ℤ)*a - 2) * dist_{𝔠 p, 4 * D^𝔰 p'} (𝒬 p') o' := hle + _ < 2^(-(5 : ℤ)*a - 2) * 2^(5*a + N + 2) := (mul_lt_mul_left (by positivity)).mpr hlt2 + _ = 2^N := by + rw [← zpow_natCast, ← zpow_add₀ two_ne_zero] + simp only [Int.reduceNeg, neg_mul, Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat, + sub_add_add_cancel, neg_add_cancel_left, zpow_natCast] + -- 6.3.12 + have hp'3 : dist_(p) (𝒬 p') o' < 2^N := by + apply lt_of_le_of_lt (cdist_mono _) hlt3 + gcongr + rw [div_le_iff₀ (by positivity)] + rw [mul_comm, ← mul_assoc] + calc (D : ℝ) ^ 𝔰 p + _ = 1 * (D : ℝ) ^ 𝔰 p := by rw [one_mul] + _ ≤ 4 * 2 ^ (2 - 5 * (a : ℤ) ^ 2 - 2 * ↑a) * D * D ^ 𝔰 p := by + have h4 : (4 : ℝ) = 2^(2 : ℤ) := by ring + apply mul_le_mul _ (le_refl _) (by positivity) (by positivity) + · have h12 : (1 : ℝ) ≤ 2 := one_le_two + simp only [defaultD, Nat.cast_pow, Nat.cast_ofNat] + rw [h4, ← zpow_natCast, ← zpow_add₀ two_ne_zero, ← zpow_add₀ two_ne_zero, + ← zpow_zero (2 : ℝ)] + rw [Nat.cast_mul, Nat.cast_ofNat, Nat.cast_pow] + gcongr --uses h12 + have : (2 : ℝ)^a = 2^(a : ℤ) := by rw [@zpow_natCast] + ring_nf + nlinarith + _ = (4 * 2 ^ (2 - 5 * (a : ℤ) ^ 2 - 2 * ↑a)) * (D * D ^ 𝔰 p) := by ring + _ ≤ 4 * 2 ^ (2 - 5 * (a : ℤ) ^ 2 - 2 * ↑a) * D ^ 𝔰 p' := by + have h1D : 1 ≤ (D : ℝ) := one_le_D + nth_rewrite 1 [mul_le_mul_left (by positivity), ← zpow_one (D : ℝ), + ← zpow_add₀ (ne_of_gt (defaultD_pos _))] + gcongr + rw [add_comm] + exact hs + -- 6.3.13 (and 6.3.3.) + have h34 : (3 : ℝ) < 4 := by linarith + calc dist_(p) o' (𝒬 p) + _ = dist_(p) (𝒬 p) o' := by rw [dist_comm] + _ ≤ dist_(p) (𝒬 p) (𝒬 p') + dist_(p) (𝒬 p') o' := dist_triangle _ _ _ + _ < 2^(N + 1) + 2^N := add_lt_add_of_le_of_lt hp'2 hp'3 + _ < 2^(N + 2) := by ring_nf; gcongr -- uses h34 + -- 6.3.14 -- Not needed + -- Def 6.3.15 def 𝔄_aux (𝔄 : Finset (𝔓 X)) (ϑ : Θ X) (N : ℕ) : Finset (𝔓 X) := diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex index bb753953..0f700bd0 100644 --- a/blueprint/src/chapter/main.tex +++ b/blueprint/src/chapter/main.tex @@ -3858,6 +3858,7 @@ \section{Proof of the Antichain Tile Count Lemma} \end{lemma} \begin{proof} +\leanok By \Cref{monotone-cube-metrics}, we have \begin{equation} d_{\fp}(\fcc(\fp'),\mfa) @@ -3866,7 +3867,7 @@ \section{Proof of the Antichain Tile Count Lemma} \end{equation} Together with \eqref{eqassumedismfa} and the triangle inequality, we obtain \begin{equation}\label{eqdistqpqp} - d_{\fp'}(\fcc(\fp'),\fcc(\fp))\le 2^{N+1} \, . + d_{\fp}(\fcc(\fp'),\fcc(\fp))\le 2^{N+1} \, . \end{equation} Now assume \begin{equation} @@ -3883,7 +3884,7 @@ \section{Proof of the Antichain Tile Count Lemma} Hence by the triangle inequality \begin{equation} B(\pc(\fp), 4D^{\ps(\fp')}) - \subset + \subseteq B(\pc(\fp'),8D^{\ps(\fp')})\, . \end{equation} Together with \eqref{ageo1} and monotonicity \eqref{monotonedb} of $d$