Proposition 2.0.2, split Discrete.Forests (#131)

…into `ForestComplement`, `ForestUnion` and `MainTheorem`. This aligns
the organisation of the code for discrete Carleson with the blueprint.

Carleson.lean

@@ -14,7 +14,9 @@ import Carleson.CoverByBalls
 import Carleson.Defs
 import Carleson.Discrete.Defs
 import Carleson.Discrete.ExceptionalSet
-import Carleson.Discrete.Forests
+import Carleson.Discrete.ForestComplement
+import Carleson.Discrete.ForestUnion
+import Carleson.Discrete.MainTheorem
 import Carleson.DoublingMeasure
 import Carleson.FinitaryCarleson
 import Carleson.Forest

Carleson/Defs.lean

@@ -323,6 +323,18 @@ lemma ballsCoverBalls_iterate {x : X} {d R r : ℝ} (hR : 0 < R) (hr : 0 < r) :
 
 end Iterate
 
+lemma measurable_Q₂ : Measurable fun p : X × X ↦ Q p.1 p.2 := fun s meass ↦ by
+  have : (fun p : X × X ↦ (Q p.1) p.2) ⁻¹' s = ⋃ θ ∈ Q.range, (Q ⁻¹' {θ}) ×ˢ (θ ⁻¹' s) := by
+    ext ⟨x, y⟩
+    simp only [mem_preimage, SimpleFunc.mem_range, mem_range, iUnion_exists, iUnion_iUnion_eq',
+      mem_iUnion, mem_prod, mem_singleton_iff]
+    constructor <;> intro h
+    · use x
+    · obtain ⟨j, hj⟩ := h; exact congr($(hj.1) y).symm ▸ hj.2
+  rw [this]
+  exact Q.range.measurableSet_biUnion fun θ _ ↦
+    (Q.measurableSet_fiber θ).prod (meass.preimage (map_continuous θ).measurable)
+
 variable (X) in
 lemma S_spec [PreProofData a q K σ₁ σ₂ F G] : ∃ n : ℕ, ∀ x, -n ≤ σ₁ x ∧ σ₂ x ≤ n := sorry
 

Carleson/Discrete/Defs.lean

@@ -234,6 +234,9 @@ lemma G₁_empty (hF : volume F = 0) : G₁ = (∅ : Set X) := by
 lemma G₁_empty' (hG : volume G = 0) : G₁ = (∅ : Set X) := by
   simp [G₁, highDensityTiles_empty' hG]
 
+lemma measurable_G₁ : MeasurableSet (G₁ (X := X)) :=
+  Finite.measurableSet_biUnion highDensityTiles.toFinite fun _ _ ↦ coeGrid_measurable
+
 /-- The set `A(λ, k, n)`, defined in (5.1.26). -/
 def setA (l k n : ℕ) : Set X :=
   {x : X | l * 2 ^ (n + 1) < stackSize (𝔐 (X := X) k n) x }
@@ -264,11 +267,22 @@ def MsetA (l k n : ℕ) : Finset (Grid X) := { j | (j : Set X) ⊆ setA l k n }
 /-- The set `G₂`, defined in (5.1.27). -/
 def G₂ : Set X := ⋃ (n : ℕ) (k ≤ n), setA (2 * n + 6) k n
 
+lemma measurable_G₂ : MeasurableSet (G₂ (X := X)) := by
+  iterate 3 refine MeasurableSet.iUnion fun _ ↦ ?_
+  exact measurable_setA
+
 /-- The set `G₃`, defined in (5.1.28). -/
 def G₃ : Set X := ⋃ (n : ℕ) (k ≤ n) (j ≤ 2 * n + 3) (p ∈ 𝔏₄ (X := X) k n j), 𝓘 p
 
+lemma measurable_G₃ : MeasurableSet (G₃ (X := X)) := by
+  iterate 7 refine MeasurableSet.iUnion fun _ ↦ ?_
+  exact coeGrid_measurable
+
 /-- The set `G'`, defined below (5.1.28). -/
 def G' : Set X := G₁ ∪ G₂ ∪ G₃
 
+lemma measurable_G' : MeasurableSet (G' (X := X)) :=
+  (measurable_G₁.union measurable_G₂).union measurable_G₃
+
 /-- The set `𝔓₁`, defined in (5.1.30). -/
 def 𝔓₁ : Set (𝔓 X) := ⋃ (n : ℕ) (k ≤ n) (j ≤ 2 * n + 3), ℭ₅ k n j

Carleson/Discrete/MainTheorem.lean

@@ -0,0 +1,39 @@
+import Carleson.Discrete.ExceptionalSet
+import Carleson.Discrete.ForestComplement
+import Carleson.Discrete.ForestUnion
+
+open MeasureTheory NNReal Set Classical
+open scoped ShortVariables
+variable {X : Type*} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X}
+  [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q D κ S o]
+
+/-! ## Proposition 2.0.2 -/
+
+/-- The constant used in Proposition 2.0.2,
+which has value `2 ^ (440 * a ^ 3) / (q - 1) ^ 5` in the blueprint. -/
+noncomputable def C2_0_2 (a : ℝ) (q : ℝ≥0) : ℝ≥0 := C5_1_2 a q + C5_1_3 a q
+
+lemma C2_0_2_pos : C2_0_2 a nnq > 0 := add_pos C5_1_2_pos C5_1_3_pos
+
+variable (X) in
+theorem discrete_carleson :
+    ∃ G', MeasurableSet G' ∧ 2 * volume G' ≤ volume G ∧
+    ∀ f : X → ℂ, Measurable f → (∀ x, ‖f x‖ ≤ F.indicator 1 x) →
+    ∫⁻ x in G \ G', ‖carlesonSum univ f x‖₊ ≤
+    C2_0_2 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹ := by
+  have exc := exceptional_set (X := X)
+  rw [zpow_neg_one, ← ENNReal.div_eq_inv_mul] at exc
+  use G', measurable_G', ENNReal.mul_le_of_le_div' exc; intro f measf hf
+  calc
+    _ ≤ ∫⁻ x in G \ G', ‖carlesonSum 𝔓₁ f x‖₊ + ‖carlesonSum 𝔓₁ᶜ f x‖₊ := by
+      refine setLIntegral_mono (by fun_prop) fun x _ ↦ ?_
+      norm_cast
+      rw [carlesonSum, ← Finset.sum_filter_add_sum_filter_not _ (· ∈ 𝔓₁ (X := X))]
+      simp_rw [Finset.filter_filter, mem_univ, true_and, carlesonSum, mem_compl_iff]
+      exact nnnorm_add_le ..
+    _ = (∫⁻ x in G \ G', ‖carlesonSum 𝔓₁ f x‖₊) + ∫⁻ x in G \ G', ‖carlesonSum 𝔓₁ᶜ f x‖₊ :=
+      lintegral_add_left (by fun_prop) _
+    _ ≤ C5_1_2 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹ +
+        C5_1_3 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹ :=
+      add_le_add (forest_union hf) (forest_complement hf)
+    _ = _ := by simp_rw [mul_assoc, ← add_mul]; congr

Carleson/FinitaryCarleson.lean

@@ -1,4 +1,4 @@
-import Carleson.Discrete.Forests
+import Carleson.Discrete.MainTheorem
 import Carleson.TileExistence
 
 open MeasureTheory Measure NNReal Metric Complex Set Classical

Carleson/TileStructure.lean

@@ -88,6 +88,15 @@ lemma cball_disjoint {p p' : 𝔓 X} (h : p ≠ p') (hp : 𝓘 p = 𝓘 p') :
 def E (p : 𝔓 X) : Set X :=
   { x ∈ 𝓘 p | Q x ∈ Ω p ∧ 𝔰 p ∈ Icc (σ₁ x) (σ₂ x) }
 
+lemma measurableSet_E {p : 𝔓 X} : MeasurableSet (E p) := by
+  refine (Measurable.and ?_ (Measurable.and ?_ ?_)).setOf
+  · rw [← measurableSet_setOf]; exact coeGrid_measurable
+  · simp_rw [← mem_preimage, ← measurableSet_setOf]; exact SimpleFunc.measurableSet_preimage ..
+  · apply (measurable_set_mem _).comp
+    apply Measurable.comp (f := fun x ↦ (σ₁ x, σ₂ x)) (g := fun p ↦ Icc p.1 p.2)
+    · exact measurable_from_prod_countable fun _ _ _ ↦ trivial
+    · exact measurable_σ₁.prod_mk measurable_σ₂
+
 section T
 
 /-- The operator `T_𝔭` defined in Proposition 2.0.2, considered on the set `F`.
@@ -97,12 +106,31 @@ def carlesonOn (p : 𝔓 X) (f : X → ℂ) : X → ℂ :=
   indicator (E p)
     fun x ↦ ∫ y, exp (I * (Q x y - Q x x)) * K x y * ψ (D ^ (- 𝔰 p) * dist x y) * f y
 
+lemma measurable_carlesonOn {p : 𝔓 X} {f : X → ℂ} (measf : Measurable f) :
+    Measurable (carlesonOn p f) := by
+  refine (StronglyMeasurable.integral_prod_right ?_).measurable.indicator measurableSet_E
+  refine (((Measurable.mul ?_ measurable_K_right).mul ?_).mul ?_).stronglyMeasurable
+  · have : Measurable fun (p : X × X) ↦ (p.1, p.1) := by fun_prop
+    refine ((Measurable.sub ?_ ?_).const_mul I).cexp <;> apply measurable_ofReal.comp
+    · exact measurable_Q₂
+    · exact measurable_Q₂.comp this
+  · apply measurable_ofReal.comp
+    apply Measurable.comp (f := fun x : X × X ↦ D ^ (-𝔰 p) * dist x.1 x.2) (g := ψ)
+    · exact measurable_const.max (measurable_const.min (Measurable.min (by fun_prop) (by fun_prop)))
+    · exact measurable_dist.const_mul _
+  · exact measf.comp measurable_snd
+
 open Classical in
 /-- The operator `T_ℭ f` defined at the bottom of Section 7.4.
 We will use this in other places of the formalization as well. -/
 def carlesonSum (ℭ : Set (𝔓 X)) (f : X → ℂ) (x : X) : ℂ :=
   ∑ p ∈ {p | p ∈ ℭ}, carlesonOn p f x
 
+@[fun_prop]
+lemma measurable_carlesonSum {ℭ : Set (𝔓 X)} {f : X → ℂ} (measf : Measurable f) :
+    Measurable (carlesonSum ℭ f) :=
+  Finset.measurable_sum _ fun _ _ ↦ measurable_carlesonOn measf
+
 lemma carlesonOn_def' (p : 𝔓 X) (f : X → ℂ) : carlesonOn p f =
     indicator (E p) fun x ↦ ∫ y, Ks (𝔰 p) x y * f y * exp (I * (Q x y - Q x x)) := by
   unfold carlesonOn Ks

blueprint/src/chapter/main.tex

@@ -1991,6 +1991,7 @@ \section{Organisation of the tiles}\label{subsectilesorg}
 \end{lemma}
 
 \begin{proof}[Proof of \Cref{discrete-Carleson}]
+\leanok
 \proves{discrete-Carleson}
 \Cref{discrete-Carleson} follows by applying the
 triangle inequality to \eqref{disclesssim}