Lemma 7.1.4 (#201)

I added two theorems in the ToMathlib file. We might also consider
generalizing `sum_pow_two_le` (in PointwiseEstimate.lean) and adding it
to Mathlib; Mathlib has some results about geometric sums indexed by
naturals, but none that I could find about geometric sums indexed by
integers.

There were a few (as far as I could tell) mistakes in the blueprint,
which I fixed:

- There were a couple uninteresting typos.
- There was some confusion about the constant `C7_1_4 a`: in the
statement of the theorem, it's 10 * 2 ^ (105a^3), but at the end of the
proof, it's 2 ^ (105a^3). I changed it to 10 * 2 ^ (104a^3).
- I don't think that the step originally described in the blueprint as
"[u]sing the doubling property (1.0.8), the definition of d_p and Lemma
2.1.2" works as written. The doubling property requires x_1 to be in
B_2, which I don't think can be proven in this situation. I used the
monotonicity property (1.0.9) to make the balls big enough that this
condition holds; this requires more applications of (1.0.8) to
compensate, but the extra factors from (1.0.8) eventually get absorbed
into the constant, with the same result as originally in the blueprint.
- The proof claims that (7.1.1) says that 𝒥 is a partition of X, but
(7.1.1) actually says that 𝒥 is a partition of the union of the dyadic
cubes; I don't see any assumption that the dyadic cubes cover all of X.
I changed the reference accordingly. (I noticed that the same claim
about 𝒥 being a partition of X is made in the proof of Lemma 7.2.3, but
I didn't edit that part.)
- Toward the end, the blueprint says "we have s(L) <= s(p) for all p,"
but I think that conclusion is only valid assuming L and p are not
disjoint. That doesn't cause any problems for the proof, because we have
nondisjointness in the relevant case; I edited the blueprint to avoid
the stronger claim.

---------

Co-authored-by: Floris van Doorn <[email protected]>

Carleson/Classical/CarlesonOnTheRealLine.lean

@@ -164,42 +164,32 @@ lemma coeΘ_R (n : Θ ℝ) (x : ℝ) : n x = n * x := rfl
 lemma coeΘ_R_C (n : Θ ℝ) (x : ℝ) : (n x : ℂ) = n * x := by norm_cast
 
 lemma oscillation_control {x : ℝ} {r : ℝ} {f g : Θ ℝ} :
-    localOscillation (ball x r) (coeΘ f) (coeΘ g) ≤ dist_{x, r} f g := by
+    localOscillation (ball x r) (coeΘ f) (coeΘ g) ≤ ENNReal.ofReal (dist_{x, r} f g) := by
   by_cases r_pos : r ≤ 0
   · rw [ball_eq_empty.mpr r_pos]
-    unfold localOscillation
-    simp [dist_nonneg]
+    simp [localOscillation, norm_nonneg]
   push_neg at r_pos
-  rw [dist_integer_linear_eq]
-  calc ⨆ z ∈ ball x r ×ˢ ball x r, |↑f * z.1 - ↑g * z.1 - ↑f * z.2 + ↑g * z.2|
-    _ = ⨆ z ∈ ball x r ×ˢ ball x r, ‖(f - g) * (z.1 - x) - (f - g) * (z.2 - x)‖ := by
+  simp_rw [dist_integer_linear_eq]
+  calc ⨆ z ∈ ball x r ×ˢ ball x r, ENNReal.ofReal ‖↑f * z.1 - ↑g * z.1 - ↑f * z.2 + ↑g * z.2‖
+    _ = ⨆ z ∈ ball x r ×ˢ ball x r, ENNReal.ofReal |(f - g) * (z.1 - x) - (f - g) * (z.2 - x)| := by
       congr with z
       congr with h
       rw [Real.norm_eq_abs]
       ring_nf
-    _ ≤ 2 * r * |↑f - ↑g| := by
-      apply Real.iSup_le
-      --TODO: investigate strange (delaborator) behavior - why is there still a sup?
-      on_goal 1 => intro z
-      on_goal 1 => apply Real.iSup_le
-      · intro hz
-        simp only [Set.mem_prod, mem_ball] at hz
-        rw [Real.dist_eq, Real.dist_eq] at hz
-        rw [Real.norm_eq_abs]
-        calc |(f - g) * (z.1 - x) - (f - g) * (z.2 - x)|
+    _ ≤ ENNReal.ofReal (2 * r * |↑f - ↑g|) := by
+      refine iSup₂_le (fun z hz ↦ ?_)
+      apply ENNReal.ofReal_le_of_le_toReal
+      rw [ENNReal.toReal_ofReal (by positivity)]
+      simp_rw [Set.mem_prod, mem_ball, Real.dist_eq] at hz
+      calc |(f - g) * (z.1 - x) - (f - g) * (z.2 - x)|
         _ ≤ |(f - g) * (z.1 - x)| + |(f - g) * (z.2 - x)| := abs_sub ..
         _ = |↑f - ↑g| * |z.1 - x| + |↑f - ↑g| * |z.2 - x| := by congr <;> apply abs_mul
         _ ≤ |↑f - ↑g| * r + |↑f - ↑g| * r := by
           gcongr
           · linarith [hz.1]
           · linarith [hz.2]
         _ = 2 * r * |↑f - ↑g| := by ring
-      all_goals
-      repeat
-        apply mul_nonneg
-        linarith
-        apply abs_nonneg
-    _ ≤ 2 * max r 0 * |↑f - ↑g| := by
+    _ ≤ ENNReal.ofReal (2 * max r 0 * |↑f - ↑g|) := by
       gcongr
       apply le_max_left
 

Carleson/Defs.lean

@@ -22,8 +22,8 @@ variable {𝕜 X : Type*} {A : ℕ} [_root_.RCLike 𝕜] [PseudoMetricSpace X]
 section localOscillation
 
 /-- The local oscillation of two functions w.r.t. a set `E`. This is `d_E` in the blueprint. -/
-def localOscillation (E : Set X) (f g : C(X, 𝕜)) : ℝ :=
-  ⨆ z ∈ E ×ˢ E, ‖f z.1 - g z.1 - f z.2 + g z.2‖
+def localOscillation (E : Set X) (f g : C(X, 𝕜)) : ℝ≥0∞ :=
+  ⨆ z ∈ E ×ˢ E, ENNReal.ofReal ‖f z.1 - g z.1 - f z.2 + g z.2‖
 
 -- example (E : Set X) (hE : IsBounded E) (f : C(X, ℝ)) :
 --     BddAbove (range fun z : E ↦ f z) := by
@@ -39,7 +39,7 @@ variable {E : Set X} {f g : C(X, 𝕜)}
 /-- A ball w.r.t. the distance `localOscillation` -/
 def localOscillationBall (E : Set X) (f : C(X, 𝕜)) (r : ℝ) :
     Set C(X, 𝕜) :=
-  { g : C(X, 𝕜) | localOscillation E f g < r }
+  { g : C(X, 𝕜) | localOscillation E f g < ENNReal.ofReal r }
 
 end localOscillation
 
@@ -95,7 +95,7 @@ class CompatibleFunctions (𝕜 : outParam Type*) (X : Type u) (A : outParam ℕ
   eq_zero : ∃ o : X, ∀ f : Θ, f o = 0
   /-- The distance is bounded below by the local oscillation. (1.0.7) -/
   localOscillation_le_cdist {x : X} {r : ℝ} {f g : Θ} :
-    localOscillation (ball x r) (coeΘ f) (coeΘ g) ≤ dist_{x, r} f g
+    localOscillation (ball x r) (coeΘ f) (coeΘ g) ≤ ENNReal.ofReal (dist_{x, r} f g)
   /-- The distance is monotone in the ball. (1.0.9) -/
   cdist_mono {x₁ x₂ : X} {r₁ r₂ : ℝ} {f g : Θ}
     (h : ball x₁ r₁ ⊆ ball x₂ r₂) : dist_{x₁, r₁} f g ≤ dist_{x₂, r₂} f g
@@ -117,6 +117,22 @@ instance nonempty_Space [CompatibleFunctions 𝕜 X A] : Nonempty X := by
 instance inhabited_Space [CompatibleFunctions 𝕜 X A] : Inhabited X :=
   ⟨nonempty_Space.some⟩
 
+lemma le_localOscillation [CompatibleFunctions 𝕜 X A] (x : X) (r : ℝ) (f g : Θ X) {y z : X}
+    (hy : y ∈ ball x r) (hz : z ∈ ball x r) : ‖coeΘ f y - coeΘ g y - coeΘ f z + coeΘ g z‖ ≤
+    ENNReal.toReal (localOscillation (ball x r) (coeΘ f) (coeΘ g)) := by
+  rw [(ENNReal.toReal_ofReal (norm_nonneg _)).symm]
+  let f (z) := ⨆ (_ : z ∈ ball x r ×ˢ ball x r), ENNReal.ofReal ‖f z.1 - g z.1 - f z.2 + g z.2‖
+  apply ENNReal.toReal_mono
+  · exact lt_of_le_of_lt CompatibleFunctions.localOscillation_le_cdist ENNReal.ofReal_lt_top |>.ne
+  · exact le_of_eq_of_le (Eq.symm (iSup_pos ⟨hy, hz⟩)) (le_iSup f ⟨y, z⟩)
+
+lemma oscillation_le_cdist [CompatibleFunctions 𝕜 X A] (x : X) (r : ℝ) (f g : Θ X) {y z : X}
+    (hy : y ∈ ball x r) (hz : z ∈ ball x r) :
+    ‖coeΘ f y - coeΘ g y - coeΘ f z + coeΘ g z‖ ≤ dist_{x, r} f g := by
+  apply le_trans <| le_localOscillation x r f g hy hz
+  rw [← ENNReal.toReal_ofReal dist_nonneg]
+  exact ENNReal.toReal_mono ENNReal.ofReal_ne_top CompatibleFunctions.localOscillation_le_cdist
+
 export CompatibleFunctions (localOscillation_le_cdist cdist_mono cdist_le le_cdist)
 
 lemma dist_congr [FunctionDistances 𝕜 X] {x₁ x₂ : X} {r₁ r₂ : ℝ} {f g : Θ X}

Carleson/DoublingMeasure.lean

@@ -47,6 +47,14 @@ lemma measure_real_ball_two_le_same (x : X) (r : ℝ) :
   · exact ENNReal.mul_ne_top coe_ne_top measure_ball_lt_top.ne
   · exact measure_ball_two_le_same x r
 
+lemma measure_real_ball_two_le_same_iterate (x : X) (r : ℝ) (n : ℕ) :
+    μ.real (ball x ((2 ^ n) * r)) ≤ A ^ n * μ.real (ball x r) := by
+  induction n with
+  | zero => simp
+  | succ m ih =>
+      simp_rw [add_comm m 1, pow_add, pow_one, mul_assoc]
+      exact le_trans (measure_real_ball_two_le_same x _) (by gcongr)
+
 lemma measure_real_ball_pos [μ.IsOpenPosMeasure] (x : X) {r : ℝ} (hr : 0 < r) :
     0 < μ.real (ball x r) :=
   toReal_pos ((measure_ball_pos μ x hr).ne.symm) (measure_ball_lt_top.ne)

Carleson/Forest.lean

@@ -65,15 +65,18 @@ lemma lt_dist (hu : u ∈ t) (hu' : u' ∈ t) (huu' : u ≠ u') {p} (hp : p ∈
 lemma ball_subset (hu : u ∈ t) (hp : p ∈ t u) : ball (𝔠 p) (8 * D ^ 𝔰 p) ⊆ 𝓘 u :=
   t.ball_subset' hu hp
 
+-- Used in the proof of Lemma 7.1.4
+variable {t} in
+lemma ball_subset_of_mem_𝓘 (hu : u ∈ t) {p : 𝔓 X} (hp : p ∈ t u) {x : X} (hx : x ∈ 𝓘 p) :
+    ball x (4 * D ^ (𝔰 p)) ⊆ 𝓘 u := by
+  refine (ball_subset_ball' ?_).trans (t.ball_subset hu hp)
+  linarith [show dist x (𝔠 p) < 4 * D ^ (𝔰 p) from Grid_subset_ball hx]
+
 lemma if_descendant_then_subset (hu : u ∈ t) (hp : p ∈ t u) : (𝓘 p : Set X) ⊆ 𝓘 u := by
   calc ↑(𝓘 p)
     _ ⊆ ball (𝔠 p) (4 * ↑D ^ 𝔰 p) := by
       exact GridStructure.Grid_subset_ball (i := 𝓘 p)
-    _ ⊆ ball (𝔠 p) (8 * ↑D ^ 𝔰 p) := by
-      gcongr
-      norm_num
-    _ ⊆ ↑(𝓘 u) := by
-      exact ball_subset t hu hp
+    _ ⊆ ↑(𝓘 u) := ball_subset_of_mem_𝓘 hu hp Grid.c_mem_Grid
 
 end Forest