From 9a3b1650d1f30b66c00afc143f6d371b942f78c7 Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Fri, 20 Sep 2024 19:29:30 +0800 Subject: [PATCH] Lemma 7.1.1, 7.1.2 and most of 7.1.5 --- Carleson/Discrete/ExceptionalSet.lean | 2 +- Carleson/ForestOperator.lean | 139 +++++++++++++++++++++++--- Carleson/GridStructure.lean | 17 +++- blueprint/src/chapter/main.tex | 2 + 4 files changed, 144 insertions(+), 16 deletions(-) diff --git a/Carleson/Discrete/ExceptionalSet.lean b/Carleson/Discrete/ExceptionalSet.lean index 5908ffee..11318a58 100644 --- a/Carleson/Discrete/ExceptionalSet.lean +++ b/Carleson/Discrete/ExceptionalSet.lean @@ -181,7 +181,7 @@ lemma dyadic_union (hx : x ∈ setA l k n) : βˆƒ i : Grid X, x ∈ i ∧ (i : Se use π“˜ b, memb.2; intro c mc; rw [mem_setOf] refine hx.trans_le (Finset.card_le_card fun y hy ↦ ?_) simp_rw [Finset.mem_filter, Finset.mem_univ, true_and] at hy ⊒ - exact ⟨hy.1, mem_of_mem_of_subset mc (Grid.le_of_mem_of_mem (minb y hy) memb.2 hy.2).1⟩ + exact ⟨hy.1, mem_of_mem_of_subset mc (le_of_mem_of_mem (minb y hy) memb.2 hy.2).1⟩ lemma iUnion_MsetA_eq_setA : ⋃ i ∈ MsetA (X := X) l k n, ↑i = setA (X := X) l k n := by ext x diff --git a/Carleson/ForestOperator.lean b/Carleson/ForestOperator.lean index ca360aab..535a3905 100644 --- a/Carleson/ForestOperator.lean +++ b/Carleson/ForestOperator.lean @@ -1,6 +1,5 @@ import Carleson.Forest import Carleson.HardyLittlewood -import Carleson.Discrete.Forests open ShortVariables TileStructure variable {X : Type*} {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} @@ -30,19 +29,23 @@ I don't think the set is always non-empty(?) -/ /-- The definition of `𝓙₀(𝔖), defined above Lemma 7.1.2 -/ def 𝓙₀ (𝔖 : Set (𝔓 X)) : Set (Grid X) := - { J : Grid X | s J = - S ∨ βˆ€ p ∈ 𝔖, Β¬ (π“˜ p : Set X) βŠ† ball (c J) (100 * D ^ (s J + 1)) } + {J : Grid X | s J = -S ∨ βˆ€ p ∈ 𝔖, Β¬(π“˜ p : Set X) βŠ† ball (c J) (100 * D ^ (s J + 1))} /-- The definition of `𝓙(𝔖), defined above Lemma 7.1.2 -/ def 𝓙 (𝔖 : Set (𝔓 X)) : Set (Grid X) := - { x | Maximal (Β· ∈ 𝓙₀ 𝔖) x} + {x | Maximal (Β· ∈ 𝓙₀ 𝔖) x} + +lemma 𝓙_subset_𝓙₀ {𝔖 : Set (𝔓 X)} : 𝓙 𝔖 βŠ† 𝓙₀ 𝔖 := sep_subset .. /-- The definition of `𝓛₀(𝔖), defined above Lemma 7.1.2 -/ def 𝓛₀ (𝔖 : Set (𝔓 X)) : Set (Grid X) := - { L : Grid X | s L = - S ∨ (βˆƒ p ∈ 𝔖, L ≀ π“˜ p) ∧ βˆ€ p ∈ 𝔖, Β¬ π“˜ p ≀ L } + {L : Grid X | s L = -S ∨ (βˆƒ p ∈ 𝔖, L ≀ π“˜ p) ∧ βˆ€ p ∈ 𝔖, Β¬π“˜ p ≀ L} /-- The definition of `𝓛(𝔖), defined above Lemma 7.1.2 -/ def 𝓛 (𝔖 : Set (𝔓 X)) : Set (Grid X) := - { x | Maximal (Β· ∈ 𝓛₀ 𝔖) x} + {x | Maximal (Β· ∈ 𝓛₀ 𝔖) x} + +lemma 𝓛_subset_𝓛₀ {𝔖 : Set (𝔓 X)} : 𝓛 𝔖 βŠ† 𝓛₀ 𝔖 := sep_subset .. /-- The projection operator `P_𝓒 f(x)`, given above Lemma 7.1.3. In lemmas the `c` will be pairwise disjoint on `C`. -/ @@ -79,25 +82,59 @@ def c𝓑 (z : β„• Γ— Grid X) : X := c z.2 def r𝓑 (z : β„• Γ— Grid X) : ℝ := 2 ^ z.1 * D ^ s z.2 /-- Lemma 7.1.1, freely translated. -/ -lemma convex_scales (hu : u ∈ t) : OrdConnected (t.Οƒ u x : Set β„€) := sorry +lemma convex_scales (hu : u ∈ t) : OrdConnected (t.Οƒ u x : Set β„€) := by + rw [ordConnected_def]; intro i mi j mj k mk + simp_rw [Finset.mem_coe, Οƒ, Finset.mem_image, Finset.mem_filter, Finset.mem_univ, + true_and] at mi mj ⊒ + obtain ⟨p, ⟨mp, xp, Qxp, sxp⟩, sp⟩ := mi + obtain ⟨p'', ⟨mp'', xp'', Qxp'', sxp''⟩, sp''⟩ := mj + have ilj : i ≀ j := nonempty_Icc.mp ⟨k, mk⟩ + rw [← sp, ← sp''] at ilj mk + obtain ⟨K, sK, lK, Kl⟩ := Grid.exists_sandwiched (le_of_mem_of_mem ilj xp xp'') k mk + have := range_subset_iff.mp (biUnion_Ξ© (i := K)) x + simp_rw [mem_preimage, mem_singleton_iff, mem_iUnion, exists_prop] at this + obtain ⟨(p' : 𝔓 X), (π“˜p' : π“˜ p' = K), Qxp'⟩ := this + rw [← π“˜p'] at lK Kl sK; refine ⟨p', ?_, sK⟩ + have l₁ : p ≀ p' := ⟨lK, + (relative_fundamental_dyadic lK).resolve_left (not_disjoint_iff.mpr ⟨_, Qxp, Qxp'⟩)⟩ + have lβ‚‚ : p' ≀ p'' := ⟨Kl, + (relative_fundamental_dyadic Kl).resolve_left (not_disjoint_iff.mpr ⟨_, Qxp', Qxp''⟩)⟩ + refine ⟨(t.ordConnected hu).out mp mp'' ⟨l₁, lβ‚‚βŸ©, ⟨(Grid.le_def.mp lK).1 xp, Qxp', ?_⟩⟩ + exact Icc_subset_Icc sxp.1 sxp''.2 ⟨(Grid.le_def.mp lK).2, (Grid.le_def.mp Kl).2⟩ /-- Part of Lemma 7.1.2 -/ @[simp] lemma biUnion_𝓙 : ⋃ J ∈ 𝓙 𝔖, J = ⋃ I : Grid X, (I : Set X) := by - sorry + refine subset_antisymm (iUnionβ‚‚_subset_iUnion ..) fun x mx ↦ ?_ + simp_rw [mem_iUnion] at mx ⊒; obtain ⟨I, mI⟩ := mx + obtain ⟨J, sJ, mJ⟩ := + Grid.exists_containing_subcube _ ⟨le_rfl, (range_subset_iff.mp range_s_subset I).1⟩ mI + have : J ∈ (𝓙₀ 𝔖).toFinset := by rw [mem_toFinset]; left; exact sJ + obtain ⟨M, lM, maxM⟩ := exists_maximal_upper_bound this + simp_rw [mem_toFinset] at maxM + use M, maxM, (Grid.le_def.mp lM).1 mJ /-- Part of Lemma 7.1.2 -/ -lemma pairwiseDisjoint_𝓙 : (𝓙 𝔖).PairwiseDisjoint (fun I ↦ (I : Set X)) := by - sorry +lemma pairwiseDisjoint_𝓙 : (𝓙 𝔖).PairwiseDisjoint (fun I ↦ (I : Set X)) := fun I mI J mJ hn ↦ by + have : IsAntichain (Β· ≀ Β·) (𝓙 𝔖) := setOf_maximal_antichain _ + exact (le_or_ge_or_disjoint.resolve_left (this mI mJ hn)).resolve_left (this mJ mI hn.symm) /-- Part of Lemma 7.1.2 -/ @[simp] lemma biUnion_𝓛 : ⋃ J ∈ 𝓛 𝔖, J = ⋃ I : Grid X, (I : Set X) := by - sorry + refine subset_antisymm (iUnionβ‚‚_subset_iUnion ..) fun x mx ↦ ?_ + simp_rw [mem_iUnion] at mx ⊒; obtain ⟨I, mI⟩ := mx + obtain ⟨J, sJ, mJ⟩ := + Grid.exists_containing_subcube _ ⟨le_rfl, (range_subset_iff.mp range_s_subset I).1⟩ mI + have : J ∈ (𝓛₀ 𝔖).toFinset := by rw [mem_toFinset]; left; exact sJ + obtain ⟨M, lM, maxM⟩ := exists_maximal_upper_bound this + simp_rw [mem_toFinset] at maxM + use M, maxM, (Grid.le_def.mp lM).1 mJ /-- Part of Lemma 7.1.2 -/ -lemma pairwiseDisjoint_𝓛 : (𝓛 𝔖).PairwiseDisjoint (fun I ↦ (I : Set X)) := by - sorry +lemma pairwiseDisjoint_𝓛 : (𝓛 𝔖).PairwiseDisjoint (fun I ↦ (I : Set X)) := fun I mI J mJ hn ↦ by + have : IsAntichain (Β· ≀ Β·) (𝓛 𝔖) := setOf_maximal_antichain _ + exact (le_or_ge_or_disjoint.resolve_left (this mI mJ hn)).resolve_left (this mJ mI hn.symm) /-- The constant used in `first_tree_pointwise`. Has value `10 * 2 ^ (105 * a ^ 3)` in the blueprint. -/ @@ -116,6 +153,84 @@ lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L (hf : IsBounded (range f)) (h2f : HasCompactSupport f) : β€–βˆ‘ i in t.Οƒ u x, ∫ y, Ks i x y * approxOnCube (𝓙 (t u)) f yβ€–β‚Š ≀ nontangentialMaximalFunction (𝒬 u) (approxOnCube (𝓙 (t u)) f) x' := by + rcases (t.Οƒ u x).eq_empty_or_nonempty with hne | hne; Β· simp [hne] + let s₁ := Finset.min' (t.Οƒ u x) hne + have ms₁ : s₁ ∈ t.Οƒ u x := Finset.min'_mem .. + simp_rw [Οƒ, Finset.mem_image, Finset.mem_filter, Finset.mem_univ, true_and] at ms₁ + obtain ⟨p, ⟨mp, xp, Qxp, sxp⟩, sp⟩ := ms₁ + have Lle : L ≀ π“˜ p := by + rcases 𝓛_subset_𝓛₀ hL with hL | hL + Β· exact le_of_mem_of_mem (hL.symm β–Έ (range_subset_iff.mp range_s_subset (π“˜ p)).1) hx xp + Β· exact (le_or_ge_of_mem_of_mem xp hx).resolve_left (hL.2 p mp) + let sβ‚‚ := Finset.max' (t.Οƒ u x) hne + have msβ‚‚ : sβ‚‚ ∈ t.Οƒ u x := Finset.max'_mem .. + simp_rw [Οƒ, Finset.mem_image, Finset.mem_filter, Finset.mem_univ, true_and] at msβ‚‚ + obtain ⟨p', ⟨mp', xp', Qxp', sxp'⟩, sp'⟩ := msβ‚‚ + have s_ineq : 𝔰 p ≀ 𝔰 p' := by + rw [sp, sp']; exact (t.Οƒ u x).min'_le sβ‚‚ (Finset.max'_mem ..) + have pinc : π“˜ p ≀ π“˜ p' := le_of_mem_of_mem s_ineq xp xp' + have d5 : dist_(p') (𝒬 u) (Q x) < 5 := + calc + _ ≀ dist_(p') (𝒬 u) (𝒬 p') + dist_(p') (Q x) (𝒬 p') := dist_triangle_right .. + _ < 4 + 1 := + add_lt_add_of_lt_of_lt ((t.smul_four_le' hu mp').2 (by convert mem_ball_self zero_lt_one)) + (subset_cball Qxp') + _ = _ := by norm_num + have d5' : dist_{x, D ^ sβ‚‚} (𝒬 u) (Q x) < 5 * defaultA a ^ 5 := by + have i1 : dist x (𝔠 p) < 4 * D ^ 𝔰 p' := + (mem_ball.mp (Grid_subset_ball xp)).trans_le <| + mul_le_mul_of_nonneg_left (zpow_le_of_le one_le_D s_ineq) zero_le_four + have i2 : dist (𝔠 p') (𝔠 p) < 4 * D ^ 𝔰 p' := + mem_ball'.mp (ball_subset_Grid.trans (Grid.le_def.mp pinc).1 |>.trans Grid_subset_ball <| + mem_ball_self (by unfold defaultD; positivity)) + calc + _ ≀ dist_{𝔠 p, 8 * D ^ 𝔰 p'} (𝒬 u) (Q x) := by + refine cdist_mono (ball_subset_ball' ?_); rw [← sp'] + calc + _ ≀ (D : ℝ) ^ 𝔰 p' + 4 * D ^ 𝔰 p' := add_le_add_left i1.le _ + _ = 5 * D ^ 𝔰 p' := by ring + _ ≀ _ := by gcongr; norm_num + _ ≀ defaultA a * dist_{𝔠 p', 4 * D ^ 𝔰 p'} (𝒬 u) (Q x) := by + convert cdist_le (xβ‚‚ := 𝔠 p) _ using 1 + Β· exact dist_congr rfl (by ring) + Β· apply i2.trans_le; nth_rw 1 [← one_mul (4 * _)]; gcongr; exact one_le_two + _ ≀ defaultA a ^ 5 * dist_(p') (𝒬 u) (Q x) := by + rw [pow_succ', mul_assoc]; gcongr + convert cdist_le_iterate _ (𝒬 u) (Q x) 4 using 1 + Β· exact dist_congr rfl (by ring) + Β· unfold defaultD; positivity + _ < _ := by rw [mul_comm]; gcongr + have d1 : dist_{x, D ^ (sβ‚‚ - 1)} (𝒬 u) (Q x) < 1 := by + have := le_cdist_iterate (x := x) (r := D ^ (sβ‚‚ - 1)) (by sorry) (𝒬 u) (Q x) (100 * a) + calc + _ ≀ dist_{x, D ^ sβ‚‚} (𝒬 u) (Q x) * 2 ^ (-100 * a : β„€) := by + rw [neg_mul, zpow_neg, le_mul_inv_iffβ‚€ (by positivity), mul_comm] + convert le_cdist_iterate _ (𝒬 u) (Q x) (100 * a) using 1 + Β· apply dist_congr rfl + rw [Nat.cast_npow, ← pow_mul, show a * (100 * a) = 100 * a ^ 2 by ring, ← Nat.cast_npow] + change _ = (D : ℝ) * _ + rw [← zpow_one_addβ‚€ (defaultD_pos _).ne', add_sub_cancel] + Β· unfold defaultD; positivity + _ < 5 * defaultA a ^ 5 * 2 ^ (-100 * a : β„€) := by gcongr + _ = 5 * (2 : ℝ) ^ (-95 * a : β„€) := by + rw [Nat.cast_npow, ← pow_mul, ← zpow_natCast, show (2 : β„•) = (2 : ℝ) by rfl, mul_assoc, + ← zpow_addβ‚€ two_ne_zero]; congr; omega + _ ≀ 5 * 2 ^ (-3 : β„€) := by + gcongr + Β· exact one_le_two + Β· linarith [four_le_a X] + _ < _ := by norm_num + have x'p : x' ∈ π“˜ p := (Grid.le_def.mp Lle).1 hx' + simp_rw [nontangentialMaximalFunction] + -- ... + refine le_iSupβ‚‚_of_le (π“˜ p) x'p <| le_iSupβ‚‚_of_le x xp ?_ + by_cases fl2 : 𝔰 p = S + Β· change _ ≀ ⨆ sβ‚‚ ∈ Ioc (𝔰 p) S, _ + simp_rw [fl2, Ioc_self] + simp only [mem_empty_iff_false, not_false_eq_true, iSup_neg, bot_eq_zero', ciSup_const, + nonpos_iff_eq_zero, ENNReal.coe_eq_zero, nnnorm_eq_zero] + -- βˆ‘ x_1 ∈ t.Οƒ u x, ∫ (y : X), Ks x_1 x y * approxOnCube (𝓙 (t.𝔗 u)) f y = 0 + sorry sorry /-- The constant used in `third_tree_pointwise`. diff --git a/Carleson/GridStructure.lean b/Carleson/GridStructure.lean index 4c2c2400..3f1691b5 100644 --- a/Carleson/GridStructure.lean +++ b/Carleson/GridStructure.lean @@ -81,6 +81,12 @@ lemma le_or_ge_or_disjoint : i ≀ j ∨ j ≀ i ∨ Disjoint (i : Set X) (j : S Β· have := le_or_disjoint h; tauto Β· have := le_or_disjoint h.le; tauto +lemma le_or_ge_of_mem_of_mem {c : X} (mi : c ∈ i) (mj : c ∈ j) : i ≀ j ∨ j ≀ i := + (or_assoc.mpr le_or_ge_or_disjoint).resolve_right (not_disjoint_iff.mpr ⟨c, mi, mj⟩) + +lemma le_of_mem_of_mem (h : s i ≀ s j) {c : X} (mi : c ∈ i) (mj : c ∈ j) : i ≀ j := + ⟨(fundamental_dyadic h).resolve_right (not_disjoint_iff.mpr ⟨c, mi, mj⟩), h⟩ + lemma eq_or_disjoint (hs : s i = s j) : i = j ∨ Disjoint (i : Set X) (j : Set X) := Or.elim (le_or_disjoint hs.le) (fun ij ↦ Or.elim (le_or_disjoint hs.ge) (fun ji ↦ Or.inl (le_antisymm ij ji)) (fun h ↦ Or.inr h.symm)) (fun h ↦ Or.inr h) @@ -139,9 +145,6 @@ lemma c_mem_Grid {i : Grid X} : c i ∈ (i : Set X) := by lemma nonempty (i : Grid X) : (i : Set X).Nonempty := ⟨c i, c_mem_Grid⟩ -lemma le_of_mem_of_mem {i j : Grid X} (h : s i ≀ s j) {c : X} (mi : c ∈ i) (mj : c ∈ j) : i ≀ j := - ⟨(fundamental_dyadic h).resolve_right (not_disjoint_iff.mpr ⟨c, mi, mj⟩), h⟩ - lemma le_dyadic {i j k : Grid X} (h : s i ≀ s j) (li : k ≀ i) (lj : k ≀ j) : i ≀ j := by obtain ⟨c, mc⟩ := k.nonempty exact le_of_mem_of_mem h (mem_of_mem_of_subset mc li.1) (mem_of_mem_of_subset mc lj.1) @@ -201,6 +204,14 @@ lemma succ_le_of_lt (h : i < j) : i.succ ≀ j := by Β· simp only [k, succ, dite_true]; exact h.le Β· exact (succ_spec k).2 j h +lemma exists_containing_subcube (l : β„€) (h : l ∈ Icc (-S : β„€) (s i)) {x : X} (mx : x ∈ i) : + βˆƒ j, s j = l ∧ x ∈ j := by + obtain ⟨lb, ub⟩ := h + rcases ub.eq_or_lt with ub | ub; Β· exact ⟨i, ub.symm, mx⟩ + have := Grid_subset_biUnion l ⟨lb, ub⟩ mx + simp_rw [mem_iUnionβ‚‚, mem_preimage, mem_singleton_iff, exists_prop] at this + exact this + lemma exists_supercube (l : β„€) (h : l ∈ Icc (s i) S) : βˆƒ j, s j = l ∧ i ≀ j := by obtain ⟨lb, ub⟩ := h rcases ub.eq_or_lt with ub | ub; Β· exact ⟨topCube, by simpa [ub] using s_topCube, le_topCube⟩ diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex index 6f6bc7cc..2135f828 100644 --- a/blueprint/src/chapter/main.tex +++ b/blueprint/src/chapter/main.tex @@ -4198,6 +4198,7 @@ \section{The pointwise tree estimate} \end{lemma} \begin{proof} + \leanok Let $s \in \mathbb{Z}$ with $\underline{\sigma} (\fu, x) \le s \le \overline{\sigma} (\fu, x)$. By definition of $\sigma$, there exists $\fp \in \fT(\fu)$ with $\ps(\fp) = \underline{\sigma} (\fu, x)$ and $x \in E(\fp)$, and there exists $\fp'' \in \fT(\fu)$ with $\ps(\fp'') = \overline{\sigma} (\fu, x)$ and $x \in E(\fp'') \subset \scI(\fp'')$. By property \eqref{coverdyadic} of the dyadic grid, there exists a cube $I \in \mathcal{D}$ of scale $s$ with $x \in I$. By property \eqref{eq-dis-freq-cover}, there exists a tile $\fp' \in \fP(I)$ with $\tQ(x) \in \fc(\fp')$. By the dyadic property \eqref{dyadicproperty} we have $\scI(\fp) \subset \scI(\fp') \subset \scI(\fp'')$, and by \eqref{eq-freq-dyadic}, we have $\fc(\fp'') \subset \fc(\fp') \subset \fc(\fp)$. Thus $\fp \le \fp' \le\fp''$, which gives with the convexity property \eqref{forest2} of $\fT(\fu)$ that $\fp' \in \fT(\fu)$, so $s \in \sigma(\fu, x)$. \end{proof} @@ -4235,6 +4236,7 @@ \section{The pointwise tree estimate} \end{lemma} \begin{proof} + \leanok Since $\mathcal{J}(\mathfrak{S})$ is the set of inclusion maximal cubes in $\mathcal{J}_0(\mathfrak{S})$, cubes in $\mathcal{J}(\mathfrak{S})$ are pairwise disjoint by \eqref{dyadicproperty}. The same applies to $\mathcal{L}(\mathfrak{S})$. If $x \in \bigcup_{I \in \mathcal{D}} I$, then there exists by \eqref{coverdyadic} a cube $I \in \mathcal{D}$ with $x \in I$ and $s(I) = -S$. Then $I \in \mathcal{J}_0(\mathfrak{S})$. There exists an inclusion maximal cube in $\mathcal{J}_0(\mathfrak{S})$ containing $I$. This cube contains $x$ and is contained in $\mathcal{J}(\mathfrak{S})$. This shows one inclusion in \eqref{eq-J-partition}, the other one follows from $\mathcal{J}(\mathfrak{S}) \subset \mathcal{D}$.