Finish the proof of Lemma 7.1.5 + Lemma 7.4.7 (#136)

…and along the way tweak the definition of `upperRadius` to be
`ENNReal`-valued, to accommodate the possibility of the relevant set
being unbounded.

Carleson/Defs.lean

@@ -171,14 +171,15 @@ def CZOperator (K : X → X → ℂ) (r : ℝ) (f : X → ℂ) (x : X) : ℂ :=
   ∫ y in {y | dist x y ∈ Ici r}, K x y * f y
 
 /-- `R_Q(θ, x)` defined in (1.0.20). -/
-def upperRadius [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X) (x : X) : ℝ :=
-  sSup { r : ℝ | dist_{x, r} θ (Q x) < 1 }
+def upperRadius [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X) (x : X) : ℝ≥0∞ :=
+  sSup { r : ℝ≥0∞ | dist_{x, r.toReal} θ (Q x) < 1 }
 
 /-- The linearized maximally truncated nontangential Calderon Zygmund operator `T_Q^θ` -/
 def linearizedNontangentialOperator [FunctionDistances ℝ X] (Q : X → Θ X) (θ : Θ X)
     (K : X → X → ℂ) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
   ⨆ (R₁ : ℝ) (x' : X) (_ : dist x x' ≤ R₁),
-  ‖∫ y in {y | dist x' y ∈ Ioo R₁ (upperRadius Q θ x')}, K x' y * f y‖₊
+  ‖∫ y in {y | ENNReal.ofReal (dist x' y) ∈ Ioo (ENNReal.ofReal R₁) (upperRadius Q θ x')},
+    K x' y * f y‖₊
 
 /-- The maximally truncated nontangential Calderon Zygmund operator `T_*` -/
 def nontangentialOperator (K : X → X → ℂ) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
@@ -486,6 +487,10 @@ lemma DκZ_le_two_rpow_100 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F
       nth_rw 1 [← mul_one (a ^ 2), ← mul_assoc]
       gcongr; exact Nat.one_le_two_pow
 
+lemma four_le_Z [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] : 4 ≤ Z := by
+  rw [defaultZ, show 4 = 2 ^ 2 by rfl]
+  exact Nat.pow_le_pow_right zero_lt_two (by linarith [four_le_a X])
+
 variable (a) in
 /-- `D` as an element of `ℝ≥0`. -/
 def nnD : ℝ≥0 := ⟨D, by simp [D_nonneg]⟩

Carleson/ForestOperator.lean

@@ -111,7 +111,7 @@ lemma biUnion_𝓙 : ⋃ J ∈ 𝓙 𝔖, J = ⋃ I : Grid X, (I : Set X) := by
   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
+    Grid.exists_containing_subcube _ ⟨le_rfl, scale_mem_Icc.1⟩ mI
   have : J ∈ (𝓙₀ 𝔖).toFinset := by rw [mem_toFinset]; left; exact sJ
   obtain ⟨M, lM, maxM⟩ := (𝓙₀ 𝔖).toFinset.exists_le_maximal this
   simp_rw [mem_toFinset] at maxM
@@ -128,7 +128,7 @@ lemma biUnion_𝓛 : ⋃ J ∈ 𝓛 𝔖, J = ⋃ I : Grid X, (I : Set X) := by
   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
+    Grid.exists_containing_subcube _ ⟨le_rfl, scale_mem_Icc.1⟩ mI
   have : J ∈ (𝓛₀ 𝔖).toFinset := by rw [mem_toFinset]; left; exact sJ
   obtain ⟨M, lM, maxM⟩ := (𝓛₀ 𝔖).toFinset.exists_le_maximal this
   simp_rw [mem_toFinset] at maxM
@@ -152,31 +152,30 @@ lemma first_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L)
   sorry
 
 /-- Lemma 7.1.5 -/
-lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L)
-    (hf : IsBounded (range f)) (h2f : HasCompactSupport f) (h3f : AEStronglyMeasurable f) :
+lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L) (hx' : x' ∈ L) :
     ‖∑ 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₁
+  obtain ⟨p, ⟨mp, xp, _, _⟩, 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_of_mem_of_mem (hL.symm ▸ scale_mem_Icc.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₂
+  obtain ⟨p', ⟨mp', xp', Qxp', _⟩, 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))
+        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
@@ -224,9 +223,17 @@ lemma second_tree_pointwise (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈ L
         · linarith [four_le_a X]
       _ < _ := by norm_num
   have x'p : x' ∈ 𝓘 p := (Grid.le_def.mp Lle).1 hx'
-  simp_rw [nontangentialMaximalFunction]
-  -- ...
-  sorry
+  refine le_iSup₂_of_le (𝓘 p) x'p <| le_iSup₂_of_le x xp <|
+    le_iSup₂_of_le (𝔰 p') ⟨s_ineq, scale_mem_Icc.2⟩ <| le_iSup_of_le ?_ ?_
+  · have : ((D : ℝ≥0∞) ^ (𝔰 p' - 1)).toReal = D ^ (s₂ - 1) := by
+      rw [sp', ← ENNReal.toReal_zpow]; simp
+    apply le_sSup; rwa [mem_setOf, dist_congr rfl this]
+  · convert le_rfl; change (Icc (𝔰 p) _).toFinset = _; rw [sp, sp']
+    apply subset_antisymm
+    · rw [← Finset.toFinset_coe (t.σ u x), toFinset_subset_toFinset]
+      exact (convex_scales hu).out (Finset.min'_mem ..) (Finset.max'_mem ..)
+    · intro z mz; rw [toFinset_Icc, Finset.mem_Icc]
+      exact ⟨Finset.min'_le _ _ mz, Finset.le_max' _ _ mz⟩
 
 /-- The constant used in `third_tree_pointwise`.
 Has value `2 ^ (151 * a ^ 3)` in the blueprint. -/
@@ -413,11 +420,11 @@ lemma density_tree_bound2 -- some assumptions on f are superfluous
 
 /-! ## Section 7.4 except Lemmas 4-6 -/
 
-/-- The definition of `Tₚ*g(x), defined above Lemma 7.4.1 -/
+/-- The definition of `Tₚ*g(x)`, defined above Lemma 7.4.1 -/
 def adjointCarleson (p : 𝔓 X) (f : X → ℂ) (x : X) : ℂ :=
   ∫ y in E p, conj (Ks (𝔰 p) y x) * exp (.I * (Q y y - Q y x)) * f y
 
-/-- The definition of `T_ℭ*g(x), defined at the bottom of Section 7.4 -/
+/-- The definition of `T_ℭ*g(x)`, defined at the bottom of Section 7.4 -/
 def adjointCarlesonSum (ℭ : Set (𝔓 X)) (f : X → ℂ) (x : X) : ℂ :=
   ∑ p ∈ {p | p ∈ ℭ}, adjointCarleson p f x
 
@@ -441,9 +448,9 @@ lemma _root_.MeasureTheory.AEStronglyMeasurable.adjointCarleson (hf : AEStrongly
     refine aestronglyMeasurable_Ks.prod_swap
   · refine Complex.continuous_exp.comp_aestronglyMeasurable ?_
     refine .const_mul (.sub ?_ ?_) _
-    . refine Measurable.aestronglyMeasurable ?_
+    · refine Measurable.aestronglyMeasurable ?_
       fun_prop
-    . refine continuous_ofReal.comp_aestronglyMeasurable ?_
+    · refine continuous_ofReal.comp_aestronglyMeasurable ?_
       exact aestronglyMeasurable_Q₂ (X := X) |>.prod_swap
   · exact hf.snd
 
@@ -529,16 +536,60 @@ lemma adjoint_tree_control (hu : u ∈ t) (hf : IsBounded (range f)) (h2f : HasC
     simp_rw [C7_4_3, ENNReal.coe_add, ENNReal.one_rpow, mul_one, ENNReal.coe_one]
     with_reducible rfl
 
-/-- Part 2 of Lemma 7.4.7. -/
-lemma 𝔗_subset_𝔖₀ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
-    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) : t u₁ ⊆ 𝔖₀ t u₁ u₂ := by
-  sorry
-
 /-- Part 1 of Lemma 7.4.7. -/
 lemma overlap_implies_distance (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
     (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hp : p ∈ t u₁ ∪ t u₂)
-    (hpu₁ : ¬ Disjoint (𝓘 p : Set X) (𝓘 u₁)) : p ∈ 𝔖₀ t u₁ u₂ := by
-  sorry
+    (hpu₁ : ¬Disjoint (𝓘 p : Set X) (𝓘 u₁)) : p ∈ 𝔖₀ t u₁ u₂ := by
+  simp_rw [𝔖₀, mem_setOf, hp, true_and]
+  wlog plu₁ : 𝓘 p ≤ 𝓘 u₁ generalizing p
+  · have u₁lp : 𝓘 u₁ ≤ 𝓘 p := (le_or_ge_or_disjoint.resolve_left plu₁).resolve_right hpu₁
+    obtain ⟨p', mp'⟩ := t.nonempty hu₁
+    have p'lu₁ : 𝓘 p' ≤ 𝓘 u₁ := (t.smul_four_le hu₁ mp').1
+    obtain ⟨c, mc⟩ := (𝓘 p').nonempty
+    specialize this (mem_union_left _ mp') (not_disjoint_iff.mpr ⟨c, mc, p'lu₁.1 mc⟩) p'lu₁
+    exact this.trans (Grid.dist_mono (p'lu₁.trans u₁lp))
+  have four_Z := four_le_Z (X := X)
+  have four_le_Zn : 4 ≤ Z * (n + 1) := by rw [← mul_one 4]; exact mul_le_mul' four_Z (by omega)
+  have four_le_two_pow_Zn : 4 ≤ 2 ^ (Z * (n + 1) - 1) := by
+    change 2 ^ 2 ≤ _; exact Nat.pow_le_pow_right zero_lt_two (by omega)
+  have ha : (2 : ℝ) ^ (Z * (n + 1)) - 4 ≥ 2 ^ (Z * n / 2 : ℝ) :=
+    calc
+      _ ≥ (2 : ℝ) ^ (Z * (n + 1)) - 2 ^ (Z * (n + 1) - 1) := by gcongr; norm_cast
+      _ = 2 ^ (Z * (n + 1) - 1) := by
+        rw [sub_eq_iff_eq_add, ← two_mul, ← pow_succ', Nat.sub_add_cancel (by omega)]
+      _ ≥ 2 ^ (Z * n) := by apply pow_le_pow_right one_le_two; rw [mul_add_one]; omega
+      _ ≥ _ := by
+        rw [← Real.rpow_natCast]
+        apply Real.rpow_le_rpow_of_exponent_le one_le_two; rw [Nat.cast_mul]
+        exact half_le_self (by positivity)
+  rcases hp with (c : p ∈ t.𝔗 u₁) | (c : p ∈ t.𝔗 u₂)
+  · calc
+    _ ≥ dist_(p) (𝒬 p) (𝒬 u₂) - dist_(p) (𝒬 p) (𝒬 u₁) := by
+      change _ ≤ _; rw [sub_le_iff_le_add, add_comm]; exact dist_triangle ..
+    _ ≥ 2 ^ (Z * (n + 1)) - 4 := by
+      gcongr
+      · exact (t.lt_dist' hu₂ hu₁ hu.symm c (plu₁.trans h2u)).le
+      · have : 𝒬 u₁ ∈ ball_(p) (𝒬 p) 4 :=
+          (t.smul_four_le hu₁ c).2 (by convert mem_ball_self zero_lt_one)
+        rw [@mem_ball'] at this; exact this.le
+    _ ≥ _ := ha
+  · calc
+    _ ≥ dist_(p) (𝒬 p) (𝒬 u₁) - dist_(p) (𝒬 p) (𝒬 u₂) := by
+      change _ ≤ _; rw [sub_le_iff_le_add, add_comm]; exact dist_triangle_right ..
+    _ ≥ 2 ^ (Z * (n + 1)) - 4 := by
+      gcongr
+      · exact (t.lt_dist' hu₁ hu₂ hu c plu₁).le
+      · have : 𝒬 u₂ ∈ ball_(p) (𝒬 p) 4 :=
+          (t.smul_four_le hu₂ c).2 (by convert mem_ball_self zero_lt_one)
+        rw [@mem_ball'] at this; exact this.le
+    _ ≥ _ := ha
+
+/-- Part 2 of Lemma 7.4.7. -/
+lemma 𝔗_subset_𝔖₀ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂) :
+    t u₁ ⊆ 𝔖₀ t u₁ u₂ := fun p mp ↦ by
+  apply overlap_implies_distance hu₁ hu₂ hu h2u (mem_union_left _ mp)
+  obtain ⟨c, mc⟩ := (𝓘 p).nonempty
+  exact not_disjoint_iff.mpr ⟨c, mc, (t.smul_four_le hu₁ mp).1.1 mc⟩
 
 /-! ## Section 7.5 -/
 

Carleson/GridStructure.lean

@@ -91,6 +91,8 @@ lemma eq_or_disjoint (hs : s i = s j) : i = j ∨ Disjoint (i : Set X) (j : Set
   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)
 
+lemma scale_mem_Icc : s i ∈ Icc (-S : ℤ) S := mem_Icc.mp (range_s_subset ⟨i, rfl⟩)
+
 lemma volume_coeGrid_lt_top : volume (i : Set X) < ⊤ :=
   measure_lt_top_of_subset Grid_subset_ball (measure_ball_ne_top _ _)
 
@@ -104,7 +106,7 @@ namespace Grid
 protected lemma inj : Injective (fun i : Grid X ↦ ((i : Set X), s i)) := GridStructure.inj
 
 lemma le_topCube : i ≤ topCube :=
-  ⟨subset_topCube, (range_s_subset ⟨i, rfl⟩).2.trans_eq s_topCube.symm⟩
+  ⟨subset_topCube, scale_mem_Icc.2.trans_eq s_topCube.symm⟩
 
 lemma isTop_topCube : IsTop (topCube : Grid X) := fun _ ↦ le_topCube
 
@@ -216,7 +218,7 @@ lemma exists_supercube (l : ℤ) (h : l ∈ Icc (s i) S) : ∃ j, s j = l ∧ i
   obtain ⟨lb, ub⟩ := h
   rcases ub.eq_or_lt with ub | ub; · exact ⟨topCube, by simpa [ub] using s_topCube, le_topCube⟩
   obtain ⟨x, hx⟩ := i.nonempty
-  have bound_i : -S ≤ s i ∧ s i ≤ S := mem_Icc.mp (range_s_subset ⟨i, rfl⟩)
+  have bound_i : -S ≤ s i ∧ s i ≤ S := scale_mem_Icc
   have ts := Grid_subset_biUnion (X := X) (i := topCube) l (by rw [s_topCube, mem_Ico]; omega)
   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
@@ -225,7 +227,7 @@ lemma exists_supercube (l : ℤ) (h : l ∈ Icc (s i) S) : ∃ j, s j = l ∧ i
 
 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⟩)
+  have bound_q : -S ≤ s j ∧ s j ≤ S := scale_mem_Icc
   rw [mem_Icc] at hl
   obtain ⟨K, sK, lbK⟩ := exists_supercube l (by change s i ≤ _ ∧ _; omega)
   use K, sK, lbK
@@ -242,7 +244,7 @@ lemma scale_succ (h : ¬IsMax i) : s i.succ = s i + 1 := by
 
 lemma opSize_succ_lt (h : ¬IsMax i) : i.succ.opSize < i.opSize := by
   simp only [opSize, Int.lt_toNat]
-  have : s i.succ ≤ S := (mem_Icc.mp (range_s_subset ⟨i.succ, rfl⟩)).2
+  have : s i.succ ≤ S := (mem_Icc.mp scale_mem_Icc).2
   replace : 0 ≤ S - s i.succ := by omega
   rw [Int.toNat_of_nonneg this, scale_succ h]
   omega

Carleson/TileExistence.lean

@@ -2138,7 +2138,7 @@ lemma Ω_RFD {p q : 𝔓 X} (h𝓘 : 𝓘 p ≤ 𝓘 q) : Disjoint (Ω p) (Ω q)
     have nmaxJ : ¬IsMax J := by
       by_contra maxJ; rw [Grid.isMax_iff] at maxJ
       rw [maxJ, show s topCube = S from s_topCube (X := X)] at sJ
-      have : 𝔰 q ≤ S := (range_s_subset ⟨q.1, rfl⟩).2
+      have : 𝔰 q ≤ S := scale_mem_Icc.2
       omega
     have succJ : J.succ = q.1 := (Grid.succ_def nmaxJ).mpr ⟨ubJ, by change 𝔰 q = _; omega⟩
     have key : Ω q ⊆ Ω ⟨J, a⟩ := by

Carleson/ToMathlib/Misc.lean

@@ -137,6 +137,9 @@ lemma tsum_geometric_ite_eq_tsum_geometric {k c : ℕ} :
   · rw [mem_support, ne_eq, ite_eq_right_iff, Classical.not_imp] at mn
     use n - k, Nat.sub_add_cancel mn.1
 
+lemma ENNReal.toReal_zpow (x : ℝ≥0∞) (z : ℤ) : x.toReal ^ z = (x ^ z).toReal := by
+  rw [← rpow_intCast, ← toReal_rpow, Real.rpow_intCast]
+
 end ENNReal
 
 section Indicator

blueprint/src/chapter/main.tex

@@ -4394,6 +4394,7 @@ \section{The pointwise tree estimate}
 \end{lemma}
 
 \begin{proof}
+    \leanok
     Let $s_1 = \underline{\sigma}(\fu, x)$. By definition, there exists a tile $\fp \in \fT(\fu)$ with $\ps(\fp) = s_1$ and $x \in E(\fp)$. Then $x \in \scI(\fp) \cap L$. By \eqref{dyadicproperty} and the definition of $\mathcal{L}(\fT(\fu))$, it follows that $L \subset \scI(\fp)$, in particular $x' \in \scI(\fp)$, so $x \in I_{s_1}(x')$.
     Next, let $s_2 = \overline{\sigma}(\fu, x)$ and let $\fp' \in \fT(\fu)$ with $\ps(\fp') = s_2$ and $x \in E(\fp')$. Since $\fp' \in \fT(\fu)$, we have $4\fp' \lesssim \fu$. Since $\tQ(x) \in \fc(\fp')$, it follows that
     $$
@@ -5106,11 +5107,12 @@ \section{Almost orthogonality of separated trees}
 \end{lemma}
 
 \begin{proof}
+    \leanok
     Suppose first that $\fp \in \fT(\fu_1)$. Then $\scI(\fp) \subset \scI(\fu_1) \subset \scI(\fu_2)$, by \eqref{forest1}. Thus we have by the separation condition \eqref{forest5}, \eqref{eq-freq-comp-ball}, \eqref{forest1} and the triangle inequality
     \begin{align*}
         d_{\fp}(\fcc(\fu_1), \fcc(\fu_2)) &\ge d_{\fp}(\fcc(\fp), \fcc(\fu_2)) - d_{\fp}(\fcc(\fp), \fcc(\fu_1))\\
         &\ge 2^{Z(n+1)} - 4\\
-        &\ge 2^{Zn}\,,
+        &\ge 2^{Zn/2}\,,
     \end{align*}
     using that $Z= 2^{12a}\ge 4$. Hence $\fp \in \mathfrak{S}$.