Lemmas 5.2.3, 5.2.4, 5.3.4 (#56)

Carleson/DiscreteCarleson.lean

@@ -114,7 +114,7 @@ def highDensityTiles : Set (𝔓 X) :=
 /-- The exceptional set `G₁`, defined in (5.1.25). -/
 def G₁ : Set X := ⋃ (p : 𝔓 X) (_ : p ∈ highDensityTiles), 𝓘 p
 
-/-- The set `A(λ, k n)`, defined in (5.1.26). -/
+/-- The set `A(λ, k, n)`, defined in (5.1.26). -/
 def setA (l k n : ℕ) : Set X :=
   {x : X | l * 2 ^ (n + 1) < ∑ p ∈ Finset.univ.filter (· ∈ 𝔐 (X := X) k n),
     (𝓘 p : Set X).indicator 1 x }
@@ -139,20 +139,35 @@ variable {k n j l : ℕ} {p p' : 𝔓 X} {x : X}
 lemma first_exception : volume (G₁ : Set X) ≤ 2 ^ (- 4 : ℤ) * volume G := by
   sorry
 
-
 /-- Lemma 5.2.2 -/
 lemma dense_cover (k : ℕ) :
-    2 ^ (k + 1) * volume G ≤ volume (⋃ p ∈ 𝓒 (X := X) k, (p : Set X)) := by
+    volume (⋃ p ∈ 𝓒 (X := X) k, (p : Set X)) ≤ 2 ^ (k + 1) * volume G := by
   sorry
 
-
 /-- Lemma 5.2.3 -/
-lemma pairwiseDisjoint_E1 : (𝔐 (X := X) k n).PairwiseDisjoint E₁ := by
-  sorry
+lemma pairwiseDisjoint_E1 : (𝔐 (X := X) k n).PairwiseDisjoint E₁ := fun p mp p' mp' h ↦ by
+  change Disjoint _ _
+  contrapose! h
+  have h𝓘 := (Disjoint.mono (E₁_subset p) (E₁_subset p')).mt h
+  wlog hs : s (𝓘 p') ≤ s (𝓘 p) generalizing p p'
+  · rw [disjoint_comm] at h h𝓘; rw [not_le] at hs; rw [this p' mp' p mp h h𝓘 hs.le]
+  obtain ⟨x, ⟨-, mxp⟩, ⟨-, mxp'⟩⟩ := not_disjoint_iff.mp h
+  rw [mem_preimage] at mxp mxp'
+  have l𝓘 := Grid.le_def.mpr ⟨(fundamental_dyadic hs).resolve_right (disjoint_comm.not.mpr h𝓘), hs⟩
+  have sΩ := (relative_fundamental_dyadic l𝓘).resolve_left <| not_disjoint_iff.mpr ⟨_, mxp', mxp⟩
+  exact (eq_of_mem_maximals mp' (mem_of_mem_of_subset mp (maximals_subset ..)) ⟨l𝓘, sΩ⟩).symm
 
 /-- Lemma 5.2.4 -/
 lemma dyadic_union (hx : x ∈ setA l k n) : ∃ i : Grid X, x ∈ i ∧ (i : Set X) ⊆ setA l k n := by
-  sorry
+  let M : Finset (𝔓 X) := Finset.univ.filter (fun p ↦ p ∈ 𝔐 k n ∧ x ∈ 𝓘 p)
+  simp_rw [setA, mem_setOf, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_id,
+    Finset.filter_filter] at hx ⊢
+  obtain ⟨b, memb, minb⟩ := M.exists_min_image 𝔰 (Finset.card_pos.mp (zero_le'.trans_lt hx))
+  simp_rw [M, Finset.mem_filter, Finset.mem_univ, true_and] at memb minb
+  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⟩
 
 /-- Lemma 5.2.5 -/
 lemma john_nirenberg : volume (setA (X := X) l k n) ≤ 2 ^ (k + 1 - l : ℤ) * volume G := by
@@ -196,7 +211,13 @@ lemma exceptional_set : volume (G' : Set X) ≤ 2 ^ (- 2 : ℤ) * volume G := by
 
 /-- Lemma 5.3.4 -/
 lemma ordConnected_tilesAt : OrdConnected (TilesAt k : Set (𝔓 X)) := by
-  sorry
+  rw [ordConnected_def]; intro p mp p'' mp'' p' mp'
+  simp_rw [TilesAt, mem_preimage, 𝓒, mem_diff, aux𝓒, mem_setOf] at mp mp'' ⊢
+  constructor
+  · obtain ⟨J, hJ, _⟩ := mp''.1
+    use J, mp'.2.1.trans hJ
+  · push_neg at mp ⊢
+    exact fun J hJ ↦ mp.2 J (mp'.1.1.trans hJ)
 
 /-- Lemma 5.3.5 -/
 lemma ordConnected_C : OrdConnected (ℭ k n : Set (𝔓 X)) := by

Carleson/GridStructure.lean

@@ -121,16 +121,19 @@ 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)
+
 @[simp] lemma lt_def {i j : Grid X} : i < j ↔ (i : Set X) ⊆ (j : Set X) ∧ s i < s j := by
   constructor <;> intro h
-  · obtain ⟨a₁, a₂⟩ := le_def.mp h.le
+  · obtain ⟨a₁, a₂⟩ := h.le
     refine ⟨a₁, lt_of_le_of_ne a₂ ?_⟩
     by_contra a₃
-    have k : (j : Set X) ⊆ i := by
-      apply (fundamental_dyadic a₃.ge).resolve_right
-      obtain ⟨c, mc⟩ := i.nonempty
-      rw [not_disjoint_iff]; use c, mem_of_mem_of_subset mc a₁, mc
-    have l := h.trans_le (le_def.mpr ⟨k, a₃.ge⟩)
+    have l : i < i := h.trans_le (le_dyadic a₃.ge h.le le_rfl)
     rwa [lt_self_iff_false] at l
   · apply lt_of_le_of_ne (le_def.mpr ⟨h.1, h.2.le⟩)
     by_contra a; rw [a, lt_self_iff_false] at h; exact h.2
@@ -146,15 +149,10 @@ lemma exists_unique_succ (i : Grid X) (h : ¬IsMax i) :
   obtain ⟨j, mj, hj⟩ := incs.exists_minimal ine
   simp only [gt_iff_lt, Finset.mem_filter, Finset.mem_univ, true_and, incs] at mj hj
   replace hj : ∀ (x : Grid X), i < x → j ≤ x := fun x mx ↦ by
-    have nlt := hj x mx
-    have nd : ¬Disjoint (j : Set X) x := by
-      obtain ⟨c, mc⟩ := i.nonempty
-      exact not_disjoint_iff.mpr ⟨c, mem_of_mem_of_subset mc (le_def.mp mj.le).1,
-        mem_of_mem_of_subset mc (le_def.mp mx.le).1⟩
     rcases lt_or_le (s x) (s j) with c | c
-    · have := (le_or_disjoint c.le).resolve_right (by rwa [disjoint_comm])
-      exact (eq_of_le_of_not_lt this nlt).symm.le
-    · exact (le_or_disjoint c).resolve_right nd
+    · have := le_dyadic c.le mx.le mj.le
+      exact (eq_of_le_of_not_lt this (hj x mx)).symm.le
+    · exact le_dyadic c mj.le mx.le
   use j, ⟨mj, hj⟩, fun k ⟨hk₁, hk₂⟩ ↦ le_antisymm (hk₂ j mj) (hj k hk₁)
 
 open Classical in
@@ -194,27 +192,23 @@ lemma exists_supercube (l : ℤ) (h : l ∈ Icc (s i) S) : ∃ j, s j = l ∧ i
   have := mem_of_mem_of_subset hx ((le_topCube (i := i)).1.trans ts)
   simp_rw [mem_preimage, mem_singleton_iff, mem_iUnion, exists_prop] at this
   obtain ⟨j, (sj : s j = l), mj⟩ := this; use j, sj
-  exact (le_or_disjoint (by omega)).resolve_right (not_disjoint_iff.mpr ⟨x, hx, mj⟩)
+  exact le_of_mem_of_mem (by omega) hx mj
 
 lemma exists_sandwiched (h : i ≤ j) (l : ℤ) (hl : l ∈ Icc (s i) (s j)) :
     ∃ k, s k = l ∧ i ≤ k ∧ k ≤ j := by
   have bound_q : -S ≤ s j ∧ s j ≤ S := mem_Icc.mp (range_s_subset ⟨j, rfl⟩)
   rw [mem_Icc] at hl
   obtain ⟨K, sK, lbK⟩ := exists_supercube l (by change s i ≤ _ ∧ _; omega)
   use K, sK, lbK
-  apply (le_or_disjoint (by omega)).resolve_right
-  rw [not_disjoint_iff]
-  obtain ⟨x, hx⟩ := i.nonempty
-  use x, mem_of_mem_of_subset hx lbK.1, mem_of_mem_of_subset hx h.1
+  exact le_dyadic (by omega) lbK h
 
 lemma scale_succ (h : ¬IsMax i) : s i.succ = s i + 1 := by
   obtain ⟨h₁, h₂⟩ := succ_spec h
   rw [lt_def] at h₁; apply le_antisymm _ (by omega)
   by_contra! h₀
   obtain ⟨z, hz₁, hz₂, hz₃⟩ :=
     exists_sandwiched (le_succ (i := i)) (s i + 1) (by rw [mem_Icc]; omega)
-  have l := (lt_def.mpr ⟨(le_def.mp hz₃).1, hz₁.symm ▸ h₀⟩).trans_le
-    (h₂ z (lt_def.mpr ⟨(le_def.mp hz₂).1, by omega⟩))
+  have l := (lt_def.mpr ⟨hz₃.1, hz₁.symm ▸ h₀⟩).trans_le (h₂ z (lt_def.mpr ⟨hz₂.1, by omega⟩))
   rwa [lt_self_iff_false] at l
 
 lemma opSize_succ_lt (h : ¬IsMax i) : i.succ.opSize < i.opSize := by
@@ -235,14 +229,10 @@ termination_by i => i.opSize
 
 lemma succ_def (h : ¬IsMax i) : i.succ = j ↔ i ≤ j ∧ s j = s i + 1 := by
   refine ⟨fun k ↦ by subst k; exact ⟨le_succ, scale_succ h⟩, fun ⟨h₁, _⟩ ↦ ?_⟩
-  replace h₁ : i < j := lt_def.mpr ⟨(le_def.mp h₁).1, by omega⟩
+  replace h₁ : i < j := lt_def.mpr ⟨h₁.1, by omega⟩
   refine succ_unique h h₁ fun j' hj' ↦ ?_
-  have b₁ : s i < s j' := (lt_def.mp hj').2
-  have b₂ : s j ≤ s j' := by omega
-  apply (le_or_disjoint b₂).resolve_right
-  obtain ⟨c, mc⟩ := i.nonempty
-  exact not_disjoint_iff.mpr ⟨c, mem_of_mem_of_subset mc (le_def.mp h₁.le).1,
-    mem_of_mem_of_subset mc (le_def.mp hj'.le).1⟩
+  have : s i < s j' := (lt_def.mp hj').2
+  exact le_dyadic (by omega) h₁.le hj'.le
 
 
 lemma dist_congr {x₁ x₂ : X} {r₁ r₂ : ℝ} {f g : Θ X} (e₁ : x₁ = x₂) (e₂ : r₁ = r₂) :

Carleson/TileExistence.lean

@@ -501,11 +501,7 @@ lemma Ω_RFD {p q : 𝔓 X} (h𝓘 : 𝓘 p ≤ 𝓘 q) : Disjoint (Ω p) (Ω q)
   · rw [or_iff_not_imp_left]; intro hi
     obtain ⟨I, y⟩ := p
     obtain ⟨J, z⟩ := q
-    have hij : I = J := by
-      refine le_antisymm h𝓘 <| Grid.le_def.mpr ⟨(fundamental_dyadic h).resolve_right ?_, h⟩
-      obtain ⟨w, mw⟩ := I.nonempty
-      rw [disjoint_comm, not_disjoint_iff]
-      use w, mw, mem_of_mem_of_subset mw (Grid.le_def.mp h𝓘).1
+    have hij : I = J := le_antisymm h𝓘 (Grid.le_dyadic h h𝓘 le_rfl)
     have k := @Ω_disjoint (p := ⟨I, y⟩) ⟨J, z⟩
     replace k : (⟨I, y⟩ : 𝔓 X) = ⟨J, z⟩ := by tauto
     rw [k]

Carleson/TileStructure.lean

@@ -143,7 +143,7 @@ lemma 𝔓.le_def' {p q : 𝔓 X} : p ≤ q ↔ 𝓘 p ≤ 𝓘 q ∧ Ω q ⊆ 
 
 lemma eq_of_𝓘_eq_𝓘_of_le (h1 : 𝓘 p = 𝓘 p') (h2 : p ≤ p') : p = p' := by
   by_contra h3
-  refine Set.disjoint_left.mp (disjoint_Ω h3 h1) (h2.2 𝒬_mem_Ω) 𝒬_mem_Ω
+  exact Set.disjoint_left.mp (disjoint_Ω h3 h1) (h2.2 𝒬_mem_Ω) 𝒬_mem_Ω
 
 lemma not_lt_of_𝓘_eq_𝓘 (h1 : 𝓘 p = 𝓘 p') : ¬ p < p' :=
   fun h2 ↦ h2.ne <| eq_of_𝓘_eq_𝓘_of_le h1 h2.le
@@ -177,23 +177,18 @@ lemma C5_3_3_le : C5_3_3 a ≤ 11 / 10 := by
   exact C2_1_2_le_inv_512 X |>.trans <| by norm_num
 
 /-- Lemma 5.3.3, Equation (5.3.3) -/
-lemma wiggle_order_11_10 {n : ℝ} (hp : p ≤ p') (hn : C5_3_3 a ≤ n) :
-    smul n p ≤ smul n p' := by
+lemma wiggle_order_11_10 {n : ℝ} (hp : p ≤ p') (hn : C5_3_3 a ≤ n) : smul n p ≤ smul n p' := by
   rcases eq_or_ne (𝓘 p) (𝓘 p') with h | h
   · rcases eq_or_ne p p' with rfl | h2
     · rfl
-    · exfalso
-      exact h2 <| eq_of_𝓘_eq_𝓘_of_le h hp
+    · exact absurd (eq_of_𝓘_eq_𝓘_of_le h hp) h2
   · calc
       _ ≤ smul (1 + C2_1_2 a * n) p := by
         apply smul_mono_left
-        rw [← le_sub_iff_add_le]
-        conv_rhs => left; rw [← one_mul n]
-        rw [C5_3_3] at hn
-        simp_rw [← sub_mul, ← inv_pos_le_iff_one_le_mul' <| sub_pos.mpr <| C2_1_2_lt_one X, hn]
-      _ ≤ smul n p' := by
-        apply smul_C2_1_2 _ (by norm_num : 0 < (5 : ℝ)⁻¹) h
-        exact smul_le_toTileLike.trans <| 𝔓.le_def.mp hp |>.trans toTileLike_le_smul
+        rwa [← le_sub_iff_add_le, ← one_sub_mul, ← inv_pos_le_iff_one_le_mul']
+        linarith [C2_1_2_le_inv_512 (X := X)]
+      _ ≤ smul n p' := smul_C2_1_2 (k := 5⁻¹) n (by norm_num) h
+        (smul_le_toTileLike.trans <| 𝔓.le_def.mp hp |>.trans toTileLike_le_smul)
 
 /-- Lemma 5.3.3, Equation (5.3.4) -/
 lemma wiggle_order_100 (hp : smul 10 p ≤ smul 1 p') (hn : 𝓘 p ≠ 𝓘 p') :
@@ -226,6 +221,11 @@ def E₁ (p : 𝔓 X) : Set X :=
 def E₂ (l : ℝ) (p : 𝔓 X) : Set X :=
   (smul l p).toSet
 
+lemma E₁_subset (p : 𝔓 X) : E₁ p ⊆ 𝓘 p := by
+  change ↑(𝓘 p) ∩ G ∩ (Q ⁻¹' Ω p) ⊆ ↑(𝓘 p)
+  rw [inter_assoc]
+  exact inter_subset_left
+
 /-! `𝔓(𝔓')` in the blueprint is `lowerClosure 𝔓'` in Lean. -/
 
 /-- This density is defined to live in `ℝ≥0∞`. Use `ENNReal.toReal` to get a real number. -/

blueprint/src/chapter/main.tex

@@ -2012,6 +2012,7 @@ \section{Proof of the Exceptional Sets Lemma}
     then $\fp=\fp'$.
 \end{lemma}
 \begin{proof}
+\leanok
 Let $\fp,\fp'$ be as in the lemma. By definition of $E_1$,
 we have
 $E_1(\fp)\subset \scI(\fp)$ and analogously for $\fp'$, we conclude from \eqref{eintersect} that $\scI(\fp)\cap \scI(\fp')\neq \emptyset$. Let without loss of generality $\scI(\fp)$ be maximal in
@@ -2035,6 +2036,7 @@ \section{Proof of the Exceptional Sets Lemma}
 \end{lemma}
 
 \begin{proof}
+\leanok
 Fix $k,n,\lambda,x$ as in the lemma such that $x\in A(\lambda,k,n)$.
 Let $\mathcal{M}$ be the set of dyadic cubes $\scI(\fp)$ with $\fp$ in $\mathfrak{M}(k,n)$ and $x\in \scI(\fp)$.
 By definition of $A(\lambda,k,n)$, the cardinality of $\mathcal{M}$ is at least $1+\lambda 2^{n+1}$.
@@ -2475,6 +2477,7 @@ \section{Auxiliary lemmas}
 \end{lemma}
 
 \begin{proof}
+    \leanok
     Suppose that $\fp \le \fp' \le \fp''$ and $\fp, \fp'' \in \fP(k)$. By \eqref{eq-defPk} we have $\scI(\fp), \scI(\fp'') \in \mathcal{C}(G,k)$, so there exists by \eqref{muhj1} some $J \in \mathcal{D}$ with
     $$
         \scI(\fp') \subset \scI(\fp'') \subset J