5.2.7

Carleson/DiscreteCarleson.lean

@@ -615,70 +615,116 @@ lemma second_exception : volume (G₂ (X := X)) ≤ 2 ^ (-4 : ℤ) * volume G :=
         ← zpow_one 2, ← ENNReal.zpow_add] <;> simp
     _ = _ := by rw [← mul_rotate, ← ENNReal.zpow_add] <;> simp
 
-/-
-_ = 2 ^ (n + 1) *
-        ((2 ^ (n + 1))⁻¹ * ∫⁻ t in Ioi 0, volume {x | t ≤ ∑ m ∈ Finset.univ.filter (· ∈ M),
-          (𝓘 m : Set X).indicator (1 : X → ℝ) x}) := by
-      rw [← mul_assoc, ENNReal.mul_inv_cancel (by simp) (by simp), one_mul]
-    _ = 2 ^ (n + 1) *
-        (∫⁻ t in Ioi 0, volume {x | t ≤ ∑ m ∈ Finset.univ.filter (· ∈ M),
-          (𝓘 m : Set X).indicator (1 : X → ℝ) x} ∂((2 : ℝ≥0∞) ^ (n + 1))⁻¹ • volume) := by
-      congr; exact (setLIntegral_smul_measure ..).symm
-    _ = 2 ^ (n + 1) *
-        ∫⁻ t in Ioi 0, volume {x | t * 2 ^ (n + 1) ≤ ∑ m ∈ Finset.univ.filter (· ∈ M),
-          (𝓘 m : Set X).indicator (1 : X → ℝ) x} := by
-      congr 1
-      sorry
--/
-
-set_option maxHeartbeats 0 in
-/-- Lemma 5.2.7 -/
-lemma top_tiles : ∑ m ∈ Finset.univ.filter (· ∈ 𝔐 (X := X) k n), volume (𝓘 m : Set X) ≤
-    2 ^ (n + k + 3) * volume G := by
+section TopTiles
+
+/-- The volume of a "layer" in the key function of Lemma 5.2.7. -/
+def layervol (k n : ℕ) (t : ℝ) : ℝ≥0∞ :=
+  volume {x | t ≤ ∑ m ∈ Finset.univ.filter (· ∈ 𝔐 (X := X) k n),
+    (𝓘 m : Set X).indicator (1 : X → ℝ) x}
+
+lemma indicator_sum_eq_natCast {s : Finset (𝔓 X)} :
+    ∑ m ∈ s, (𝓘 m : Set X).indicator (1 : X → ℝ) x =
+    Nat.cast (∑ m ∈ s, (𝓘 m : Set X).indicator (1 : X → ℕ) x) := by
+  push_cast; congr!; simp [indicator]
+
+lemma layervol_eq_zero_of_lt {t : ℝ} (ht : (𝔐 (X := X) k n).toFinset.card < t) :
+    layervol (X := X) k n t = 0 := by
+  rw [layervol, measure_zero_iff_ae_nmem]
+  refine ae_of_all volume fun x ↦ ?_; rw [mem_setOf, not_le]
+  calc
+    _ ≤ ((𝔐 (X := X) k n).toFinset.card : ℝ) := by
+      simp_rw [indicator_sum_eq_natCast, Nat.cast_le, indicator_apply, Pi.one_apply,
+        Finset.sum_boole, Nat.cast_id, filter_mem_univ_eq_toFinset]
+      exact Finset.card_le_card (Finset.filter_subset ..)
+    _ < _ := ht
+
+lemma lintegral_Ioc_layervol_one {l : ℕ} :
+    ∫⁻ t in Ioc (l : ℝ) (l + 1), layervol (X := X) k n t = layervol (X := X) k n (l + 1) :=
+  calc
+    _ = ∫⁻ t in Ioc (l : ℝ) (l + 1), layervol (X := X) k n (l + 1) := by
+      refine setLIntegral_congr_fun measurableSet_Ioc (ae_of_all volume fun t mt ↦ ?_)
+      unfold layervol; congr; ext x; simp_rw [mem_setOf]; constructor <;> intro h
+      · rw [indicator_sum_eq_natCast, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le]
+        rw [indicator_sum_eq_natCast, ← Nat.ceil_le] at h; convert h; symm
+        rwa [Nat.ceil_eq_iff (by omega), add_tsub_cancel_right, Nat.cast_add, Nat.cast_one]
+      · exact mt.2.trans h
+    _ = layervol k n (l + 1) * volume (Ioc (l : ℝ) (l + 1)) := setLIntegral_const ..
+    _ = _ := by rw [Real.volume_Ioc, add_sub_cancel_left, ENNReal.ofReal_one, mul_one]
+
+lemma antitone_layervol : Antitone fun t ↦ layervol (X := X) k n t := fun i j h ↦ by
+  unfold layervol; exact measure_mono fun x hx ↦ h.trans hx
+
+lemma lintegral_Ioc_layervol_le {a b : ℕ} : ∫⁻ t in Ioc (a : ℝ) b, layervol (X := X) k n t ≤
+    (b - a : ℕ) * layervol (X := X) k n (a + 1) := by
+  calc
+    _ = ∑ l ∈ Finset.Ico a b, ∫⁻ t in Ioc (l : ℝ) (l + 1), layervol (X := X) k n t := by
+      nth_rw 1 [← mul_one (a : ℝ), ← mul_one (b : ℝ)]
+      convert lintegral_Ioc_partition zero_le_one using 4; simp
+    _ = ∑ l ∈ Finset.Ico a b, layervol (X := X) k n (l + 1) := by
+      congr! 2; exact lintegral_Ioc_layervol_one
+    _ ≤ ∑ l ∈ Finset.Ico a b, layervol (X := X) k n (a + 1) :=
+      Finset.sum_le_sum fun l ml ↦ antitone_layervol (by simp_all)
+    _ = _ := by rw [Finset.sum_const, Nat.card_Ico, nsmul_eq_mul]
+
+lemma top_tiles_aux : ∑ m ∈ Finset.univ.filter (· ∈ 𝔐 (X := X) k n), volume (𝓘 m : Set X) =
+    ∫⁻ t in Ioc 0 ((𝔐 (X := X) k n).toFinset.card * 2 ^ (n + 1) : ℝ), layervol (X := X) k n t := by
   set M := 𝔐 (X := X) k n
-  let Mc := M.toFinset.card
-  let layervol : ℝ → ℝ≥0∞ := fun t ↦
-    volume {x | t ≤ ∑ m ∈ Finset.univ.filter (· ∈ M), (𝓘 m : Set X).indicator (1 : X → ℝ) x}
+  set Mc := M.toFinset.card
   calc
     _ = ∑ m ∈ Finset.univ.filter (· ∈ M), ∫⁻ x, (𝓘 m : Set X).indicator 1 x := by
       congr! with m; exact (lintegral_indicator_one coeGrid_measurable).symm
     _ = ∫⁻ x, ∑ m ∈ Finset.univ.filter (· ∈ M), (𝓘 m : Set X).indicator 1 x :=
       (lintegral_finset_sum _ fun _ _ ↦ measurable_one.indicator coeGrid_measurable).symm
     _ = ∫⁻ x, ENNReal.ofReal (∑ m ∈ Finset.univ.filter (· ∈ M), (𝓘 m : Set X).indicator 1 x) := by
       congr! 2 with x; rw [ENNReal.ofReal_sum_of_nonneg]
-      · congr! with m hm; simp_rw [indicator]; split_ifs <;> simp
+      · congr!; unfold indicator; split_ifs <;> simp
       · exact fun _ _ ↦ indicator_nonneg (fun _ _ ↦ by simp) _
-    _ = ∫⁻ t in Ioi 0, layervol t := by
+    _ = ∫⁻ t in Ioi 0, layervol k n t := by
       apply lintegral_eq_lintegral_meas_le
       · exact ae_of_all volume fun _ ↦
           Finset.sum_nonneg' fun _ ↦ indicator_nonneg (fun _ _ ↦ by simp) _
       · exact Measurable.aemeasurable <|
           Finset.measurable_sum _ (fun _ _ ↦ measurable_one.indicator coeGrid_measurable)
-    _ = ∫⁻ t in Ioc 0 (Mc * 2 ^ (n + 1) : ℝ), layervol t := by
+    _ = _ := by
       have nn : 0 ≤ (Mc * 2 ^ (n + 1) : ℝ) := by positivity
       rw [← Ioc_union_Ioi_eq_Ioi nn, lintegral_union measurableSet_Ioi Ioc_disjoint_Ioi_same]
       nth_rw 3 [← add_zero (lintegral ..)]; congr 1
-      have cgr : ∫⁻ (t : ℝ) in Ioi (Mc * 2 ^ (n + 1) : ℝ), layervol t =
-          ∫⁻ (t : ℝ) in Ioi (Mc * 2 ^ (n + 1) : ℝ), 0 := by
-        refine setLIntegral_congr_fun measurableSet_Ioi (ae_of_all volume fun t mt ↦ ?_)
-        simp_rw [layervol, measure_zero_iff_ae_nmem]
-        refine ae_of_all volume fun x ↦ ?_
-        rw [mem_setOf, not_le]
-        calc
-          _ = Nat.cast (∑ m ∈ Finset.univ.filter (· ∈ M),
-              (𝓘 m : Set X).indicator (1 : X → ℕ) x) := by push_cast; congr!; simp [indicator]
-          _ ≤ (Mc : ℝ) := by
-            norm_cast
-            simp_rw [indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_id,
-              filter_mem_univ_eq_toFinset, Mc]
-            exact Finset.card_le_card (Finset.filter_subset ..)
-          _ ≤ Mc * (2 ^ (n + 1)) := by
-            norm_cast; exact Nat.le_mul_of_pos_right Mc (by positivity)
-          _ < _ := mt
-      simp [cgr]
-    _ ≤ 2 ^ (n + 1) * ∑ l ∈ Finset.Icc 0 Mc, volume (setA (X := X) l k n) := by
-      sorry
-    _ ≤ 2 ^ (n + 1) * ∑ l ∈ Finset.Icc 0 Mc, 2 ^ (k + 1 - l : ℤ) * volume G :=
+      have cgr : ∫⁻ (t : ℝ) in Ioi (Mc * 2 ^ (n + 1) : ℝ), layervol (X := X) k n t =
+          ∫⁻ _ in Ioi (Mc * 2 ^ (n + 1) : ℝ), 0 := by
+        refine setLIntegral_congr_fun measurableSet_Ioi (ae_of_all volume fun t mt ↦
+          layervol_eq_zero_of_lt (lt_of_le_of_lt ?_ mt))
+        exact_mod_cast Nat.le_mul_of_pos_right Mc (by positivity)
+      rw [cgr, lintegral_zero]
+
+/-- Lemma 5.2.7 -/
+lemma top_tiles : ∑ m ∈ Finset.univ.filter (· ∈ 𝔐 (X := X) k n), volume (𝓘 m : Set X) ≤
+    2 ^ (n + k + 3) * volume G := by
+  set M := 𝔐 (X := X) k n
+  let Mc := M.toFinset.card
+  calc
+    _ = ∫⁻ t in Ioc 0 (Mc * 2 ^ (n + 1) : ℝ), layervol (X := X) k n t := top_tiles_aux
+    _ = ∑ l ∈ Finset.range Mc,
+        ∫⁻ t in Ioc ((l : ℝ) * 2 ^ (n + 1)) ((l + 1 : ℕ) * 2 ^ (n + 1)),
+          layervol (X := X) k n t := by
+      rw [Finset.range_eq_Ico, show (0 : ℝ) = (0 : ℕ) * 2 ^ (n + 1) by simp]
+      exact lintegral_Ioc_partition (by positivity)
+    _ ≤ ∑ l ∈ Finset.range Mc,
+        (((l + 1) * 2 ^ (n + 1) - l * 2 ^ (n + 1) : ℕ)) *
+          layervol (X := X) k n ((l * 2 ^ (n + 1) : ℕ) + 1) := by
+      conv_lhs =>
+        enter [2, l]
+        rw [show (l : ℝ) * 2 ^ (n + 1) = (l * 2 ^ (n + 1) : ℕ) by simp,
+          show (l + 1 : ℕ) * (2 : ℝ) ^ (n + 1) = ((l + 1) * 2 ^ (n + 1) : ℕ) by simp]
+      exact Finset.sum_le_sum fun _ _ ↦ lintegral_Ioc_layervol_le
+    _ = 2 ^ (n + 1) * ∑ l ∈ Finset.range Mc, layervol (X := X) k n (l * 2 ^ (n + 1) + 1 : ℕ) := by
+      rw [Finset.mul_sum]; congr! 2
+      · rw [← Nat.mul_sub_right_distrib]; simp
+      · congr; simp
+    _ = 2 ^ (n + 1) * ∑ l ∈ Finset.range Mc, volume (setA (X := X) l k n) := by
+      unfold layervol setA stackSize; congr! 3; ext x
+      rw [mem_setOf, mem_setOf, indicator_sum_eq_natCast, Nat.cast_le]
+      exact Nat.add_one_le_iff
+    _ ≤ 2 ^ (n + 1) * ∑ l ∈ Finset.range Mc, 2 ^ (k + 1 - l : ℤ) * volume G :=
       mul_le_mul_left' (Finset.sum_le_sum fun _ _ ↦ john_nirenberg) _
     _ ≤ 2 ^ (n + 1) * ∑' (l : ℕ), 2 ^ (k + 1 - l : ℤ) * volume G :=
       mul_le_mul_left' (ENNReal.sum_le_tsum _) _
@@ -694,7 +740,7 @@ lemma top_tiles : ∑ m ∈ Finset.univ.filter (· ∈ 𝔐 (X := X) k n), volum
       rw [mul_rotate, ← pow_add, ← mul_assoc, ← pow_add,
         show n + 1 + (k + 1 + 1) = n + k + 3 by omega]
 
-#exit
+end TopTiles
 
 /-- Lemma 5.2.8 -/
 lemma tree_count :

Carleson/ToMathlib/Misc.lean

@@ -1,6 +1,7 @@
 import Mathlib.Analysis.Convex.PartitionOfUnity
 import Mathlib.Analysis.Calculus.ContDiff.Basic
 import Mathlib.MeasureTheory.Integral.Bochner
+import Mathlib.MeasureTheory.Measure.Haar.OfBasis
 import Mathlib.Topology.MetricSpace.Holder
 import Mathlib.Data.Set.Card
 import Mathlib.Data.Real.ENatENNReal
@@ -109,6 +110,28 @@ lemma ENNReal.sum_geometric_two_pow_neg_two :
   conv_lhs => enter [1, n, 2]; rw [← Nat.cast_two]
   rw [ENNReal.sum_geometric_two_pow_toNNReal zero_lt_two]; norm_num
 
+/-! ## Partitioning an interval -/
+
+namespace MeasureTheory
+
+lemma lintegral_Ioc_partition {a b : ℕ} {c : ℝ} {f : ℝ → ℝ≥0∞} (hc : 0 ≤ c) :
+    ∫⁻ t in Ioc (a * c) (b * c), f t =
+    ∑ l ∈ Finset.Ico a b, ∫⁻ t in Ioc (l * c) ((l + 1 : ℕ) * c), f t := by
+  rcases lt_or_le b a with h | h
+  · rw [Finset.Ico_eq_empty (by omega), Ioc_eq_empty (by rw [not_lt]; gcongr),
+      setLIntegral_empty, Finset.sum_empty]
+  induction b, h using Nat.le_induction with
+  | base =>
+    rw [Finset.Ico_self, Ioc_self, setLIntegral_empty, Finset.sum_empty]
+  | succ b h ih =>
+    have li : a * c ≤ b * c := by gcongr
+    rw [← Ioc_union_Ioc_eq_Ioc li (by gcongr; omega),
+      lintegral_union measurableSet_Ioc Ioc_disjoint_Ioc_same,
+      Nat.Ico_succ_right_eq_insert_Ico h, Finset.sum_insert Finset.right_not_mem_Ico,
+      add_comm (lintegral ..), ih]
+
+end MeasureTheory
+
 /-! ## `EquivalenceOn` -/
 
 /-- An equivalence relation on the set `s`. -/