Finishing all of 4.1 and 4.0.1 (#82)

this PR completes the remaining parts of 4.1, and the key lemma which is
its purpose: 4.0.1.

i understand if this PR is too big to review all at once, but i think it
would be good to make sure that there at least is a visible branch which
has these completed. advice on where to start splitting this PR is
welcome.

this PR does not include the appropriate changes to the blueprint.

---------

Co-authored-by: Blizzard_inc <[email protected]>

Carleson/Defs.lean

@@ -291,6 +291,45 @@ variable {X : Type*} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X
 variable (X) in
 lemma S_spec [PreProofData a q K σ₁ σ₂ F G] : ∃ n : ℕ, ∀ x, -n ≤ σ₁ x ∧ σ₂ x ≤ n := sorry
 
+-- used in 4.1.7 (`small_boundary`)
+variable (X) in
+lemma twentyfive_le_realD : (25:ℝ) ≤ defaultD a := by
+  simp only [defaultD, Nat.ofNat_le_cast]
+  have : 4 ≤ a := four_le_a X
+  calc
+    (25:ℕ)
+      ≤ 32 := by linarith
+    _ = 2 ^ (5) := by norm_num
+    _ ≤ 2 ^ (100 * 4 ^ 2) := by
+      exact Nat.le_of_ble_eq_true rfl
+    _ ≤ 2 ^ (100 * a^2) := by
+      apply Nat.pow_le_pow_right (by norm_num)
+      apply mul_le_mul_of_nonneg_left _ (by norm_num)
+      exact Nat.pow_le_pow_of_le_left this 2
+
+-- used in 4.1.3 (`I3_prop_3_1`)
+variable (X) in
+lemma eight_le_realD : (8:ℝ) ≤ defaultD a := by
+  have : (25:ℝ) ≤ defaultD a := twentyfive_le_realD X
+  linarith
+
+-- used in 4.1.6 (`transitive_boundary`)
+variable (X) in
+lemma five_le_realD : (5:ℝ) ≤ defaultD a := by
+  have : (25:ℝ) ≤ defaultD a := twentyfive_le_realD X
+  linarith
+
+-- used in various places in `Carleson.TileExistence`
+variable (X) in
+lemma four_le_realD : (4:ℝ) ≤ defaultD a := by
+  have : (25:ℝ) ≤ defaultD a := twentyfive_le_realD X
+  linarith
+
+variable (X) in
+lemma one_le_realD : (1:ℝ) ≤ defaultD a := by
+  have : (25:ℝ) ≤ defaultD a := twentyfive_le_realD X
+  linarith
+
 variable (X) in
 open Classical in
 def S [PreProofData a q K σ₁ σ₂ F G] : ℕ := Nat.find (S_spec X)
@@ -353,6 +392,10 @@ lemma one_le_D : 1 ≤ (D : ℝ) := by
 
 lemma D_nonneg : 0 ≤ (D : ℝ) := zero_le_one.trans one_le_D
 
+lemma κ_nonneg : 0 ≤ κ := by
+  dsimp only [defaultκ]
+  exact Real.rpow_nonneg (by norm_num) _
+
 variable (a) in
 /-- `D` as an element of `ℝ≥0`. -/
 def nnD : ℝ≥0 := ⟨D, by simp [D_nonneg]⟩

Carleson/GridStructure.lean

@@ -35,8 +35,8 @@ class GridStructure
   fundamental_dyadic' {i j} : s i ≤ s j → coeGrid i ⊆ coeGrid j ∨ Disjoint (coeGrid i) (coeGrid j)
   ball_subset_Grid {i} : ball (c i) (D ^ s i / 4) ⊆ coeGrid i --2.0.10
   Grid_subset_ball {i} : coeGrid i ⊆ ball (c i) (4 * D ^ s i) --2.0.10
-  small_boundary {i} {t : ℝ} (ht : D ^ (- S - s i) ≤ t) :
-    volume.real { x ∈ coeGrid i | infDist x (coeGrid i)ᶜ ≤ t * D ^ s i } ≤ 2 * t ^ κ * volume.real (coeGrid i)
+  small_boundary {i} {t : ℝ≥0} (ht : D ^ (- S - s i) ≤ t) :
+    volume.real { x ∈ coeGrid i | EMetric.infEdist x (coeGrid i)ᶜ ≤ t * (D ^ (s i):ℝ≥0∞)} ≤ 2 * t ^ κ * volume.real (coeGrid i)
   coeGrid_measurable {i} : MeasurableSet (coeGrid i)
 
 export GridStructure (range_s_subset Grid_subset_biUnion ball_subset_Grid Grid_subset_ball small_boundary