Lemma 7.1.1, 7.1.2 and most of 7.1.5

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

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`.

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⟩

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}$.