split the ForestOperator file (#138)

Carleson.lean

@@ -20,7 +20,13 @@ import Carleson.Discrete.MainTheorem
 import Carleson.DoublingMeasure
 import Carleson.FinitaryCarleson
 import Carleson.Forest
-import Carleson.ForestOperator
+import Carleson.ForestOperator.AlmostOrthogonality
+import Carleson.ForestOperator.Forests
+import Carleson.ForestOperator.L2Estimate
+import Carleson.ForestOperator.LargeSeparation
+import Carleson.ForestOperator.PointwiseEstimate
+import Carleson.ForestOperator.QuantativeEstimate
+import Carleson.ForestOperator.RemainingTiles
 import Carleson.GridStructure
 import Carleson.HardyLittlewood
 import Carleson.HolderVanDerCorput

Carleson/ForestOperator/AlmostOrthogonality.lean

@@ -0,0 +1,188 @@
+import Carleson.ForestOperator.QuantativeEstimate
+
+open ShortVariables TileStructure
+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]
+  {n j j' : ℕ} {t : Forest X n} {u u₁ u₂ p : 𝔓 X} {x x' : X} {𝔖 : Set (𝔓 X)}
+  {f f₁ f₂ g g₁ g₂ : X → ℂ} {I J J' L : Grid X}
+variable {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E']
+
+noncomputable section
+
+open Set MeasureTheory Metric Function Complex Bornology TileStructure Classical Filter
+open scoped NNReal ENNReal ComplexConjugate
+
+namespace TileStructure.Forest
+
+/-! ## Section 7.4 except Lemmas 4-6 -/
+
+/-- 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 -/
+def adjointCarlesonSum (ℭ : Set (𝔓 X)) (f : X → ℂ) (x : X) : ℂ :=
+  ∑ p ∈ {p | p ∈ ℭ}, adjointCarleson p f x
+
+variable (t) in
+/-- The operator `S_{2,𝔲} f(x)`, given above Lemma 7.4.3. -/
+def adjointBoundaryOperator (u : 𝔓 X) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
+  ‖adjointCarlesonSum (t u) f x‖₊ + MB volume 𝓑 c𝓑 r𝓑 f x + ‖f x‖₊
+
+variable (t u₁ u₂) in
+/-- The set `𝔖` defined in the proof of Lemma 7.4.4.
+We append a subscript 0 to distinguish it from the section variable. -/
+def 𝔖₀ : Set (𝔓 X) := { p ∈ t u₁ ∪ t u₂ | 2 ^ ((Z : ℝ) * n / 2) ≤ dist_(p) (𝒬 u₁) (𝒬 u₂) }
+
+lemma _root_.MeasureTheory.AEStronglyMeasurable.adjointCarleson (hf : AEStronglyMeasurable f) :
+    AEStronglyMeasurable (adjointCarleson p f) := by
+  refine .integral_prod_right'
+    (f := fun z ↦ conj (Ks (𝔰 p) z.2 z.1) * exp (Complex.I * (Q z.2 z.2 - Q z.2 z.1)) * f z.2) ?_
+  refine .mono_ac (.prod .rfl restrict_absolutelyContinuous) ?_
+  refine .mul (.mul ?_ ?_) ?_
+  · exact Complex.continuous_conj.comp_aestronglyMeasurable (aestronglyMeasurable_Ks.prod_swap)
+  · refine Complex.continuous_exp.comp_aestronglyMeasurable (.const_mul (.sub ?_ ?_) _)
+    · refine Measurable.aestronglyMeasurable ?_
+      fun_prop
+    · refine continuous_ofReal.comp_aestronglyMeasurable ?_
+      exact aestronglyMeasurable_Q₂ (X := X) |>.prod_swap
+  · exact hf.snd
+
+lemma _root_.MeasureTheory.AEStronglyMeasurable.adjointCarlesonSum {ℭ : Set (𝔓 X)}
+    (hf : AEStronglyMeasurable f) :
+    AEStronglyMeasurable (adjointCarlesonSum ℭ f) :=
+  Finset.aestronglyMeasurable_sum _ fun _ _ ↦ hf.adjointCarleson
+
+/-- Part 1 of Lemma 7.4.1.
+Todo: update blueprint with precise properties needed on the function. -/
+lemma adjoint_tile_support1 (hf : IsBounded (range f)) (h2f : HasCompactSupport f)
+    (h3f : AEStronglyMeasurable f) :
+    adjointCarleson p f =
+    (ball (𝔠 p) (5 * D ^ 𝔰 p)).indicator (adjointCarleson p ((𝓘 p : Set X).indicator f)) := by
+  sorry
+
+/-- Part 2 of Lemma 7.4.1.
+Todo: update blueprint with precise properties needed on the function. -/
+lemma adjoint_tile_support2 (hu : u ∈ t) (hp : p ∈ t u)
+    (hf : IsBounded (range f)) (h2f : HasCompactSupport f) (h3f : AEStronglyMeasurable f) :
+    adjointCarleson p f =
+    (𝓘 p : Set X).indicator (adjointCarleson p ((𝓘 p : Set X).indicator f)) := by
+  sorry
+
+/-- The constant used in `adjoint_tree_estimate`.
+Has value `2 ^ (155 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+irreducible_def C7_4_2 (a : ℕ) : ℝ≥0 := 2 ^ (155 * (a : ℝ) ^ 3)
+
+/-- Lemma 7.4.2. -/
+lemma adjoint_tree_estimate (hu : u ∈ t) (hf : IsBounded (range f)) (h2f : HasCompactSupport f)
+    (h3f : AEStronglyMeasurable f) :
+    eLpNorm (adjointCarlesonSum (t u) f) 2 volume ≤
+    C7_4_2 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 volume := by
+  sorry
+
+/-- The constant used in `adjoint_tree_control`.
+Has value `2 ^ (156 * a ^ 3)` in the blueprint. -/
+irreducible_def C7_4_3 (a : ℕ) : ℝ≥0 :=
+  C7_4_2 a + CMB (defaultA a) 2 + 1
+
+/-- Lemma 7.4.3. -/
+lemma adjoint_tree_control (hu : u ∈ t) (hf : IsBounded (range f)) (h2f : HasCompactSupport f)
+    (h3f : AEStronglyMeasurable f) :
+    eLpNorm (adjointBoundaryOperator t u f · |>.toReal) 2 volume ≤
+    C7_4_3 a * eLpNorm f 2 volume := by
+  calc _ ≤ eLpNorm (adjointBoundaryOperator t u f · |>.toReal) 2 volume := by rfl
+  _ ≤ eLpNorm
+    ((‖adjointCarlesonSum (t u) f ·‖) + (MB volume 𝓑 c𝓑 r𝓑 f · |>.toReal) + (‖f ·‖))
+    2 volume := by
+      refine MeasureTheory.eLpNorm_mono_real fun x ↦ ?_
+      simp_rw [Real.norm_eq_abs, ENNReal.abs_toReal, Pi.add_apply]
+      refine ENNReal.toReal_add_le.trans ?_
+      gcongr
+      · exact ENNReal.toReal_add_le
+      · rfl
+  _ ≤ eLpNorm (‖adjointCarlesonSum (t u) f ·‖) 2 volume +
+    eLpNorm (MB volume 𝓑 c𝓑 r𝓑 f · |>.toReal) 2 volume +
+    eLpNorm (‖f ·‖) 2 volume := by
+      refine eLpNorm_add_le ?_ ?_ one_le_two |>.trans ?_
+      · exact h3f.adjointCarlesonSum.norm.add <| .maximalFunction_toReal 𝓑_finite.countable
+      · exact h3f.norm
+      gcongr
+      refine eLpNorm_add_le ?_ ?_ one_le_two |>.trans ?_
+      · exact h3f.adjointCarlesonSum.norm
+      · exact .maximalFunction_toReal 𝓑_finite.countable
+      rfl
+  _ ≤ eLpNorm (adjointCarlesonSum (t u) f) 2 volume +
+    eLpNorm (MB volume 𝓑 c𝓑 r𝓑 f · |>.toReal) 2 volume +
+    eLpNorm f 2 volume := by simp_rw [eLpNorm_norm]; rfl
+  _ ≤ C7_4_2 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 volume +
+    CMB (defaultA a) 2 * eLpNorm f 2 volume +
+    eLpNorm f 2 volume := by
+      gcongr
+      · exact adjoint_tree_estimate hu hf h2f h3f
+      · exact hasStrongType_MB 𝓑_finite one_lt_two _ (h2f.memℒp_of_isBounded hf h3f) |>.2
+  _ ≤ (C7_4_2 a * (1 : ℝ≥0∞) ^ (2 : ℝ)⁻¹ + CMB (defaultA a) 2 + 1) * eLpNorm f 2 volume := by
+    simp_rw [add_mul]
+    gcongr
+    · exact dens₁_le_one
+    · simp only [ENNReal.coe_one, one_mul, le_refl]
+  _ ≤ C7_4_3 a * eLpNorm f 2 volume := by
+    simp_rw [C7_4_3, ENNReal.coe_add, ENNReal.one_rpow, mul_one, ENNReal.coe_one]
+    with_reducible rfl
+
+/-- 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
+  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⟩
+
+end TileStructure.Forest

Carleson/ForestOperator/Forests.lean

@@ -0,0 +1,131 @@
+import Carleson.ForestOperator.LargeSeparation
+import Carleson.ForestOperator.RemainingTiles
+
+open ShortVariables TileStructure
+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]
+  {n j j' : ℕ} {t : Forest X n} {u u₁ u₂ p : 𝔓 X} {x x' : X} {𝔖 : Set (𝔓 X)}
+  {f f₁ f₂ g g₁ g₂ : X → ℂ} {I J J' L : Grid X}
+variable {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E']
+
+noncomputable section
+
+open Set MeasureTheory Metric Function Complex Bornology TileStructure Classical Filter
+open scoped NNReal ENNReal ComplexConjugate
+
+namespace TileStructure.Forest
+
+/-! ## Lemmas 7.4.4 -/
+
+/-- The constant used in `correlation_separated_trees`.
+Has value `2 ^ (550 * a ^ 3 - 3 * n)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+irreducible_def C7_4_4 (a n : ℕ) : ℝ≥0 := 2 ^ (550 * (a : ℝ) ^ 3 - 3 * n)
+
+lemma correlation_separated_trees_of_subset (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (h2u : 𝓘 u₁ ≤ 𝓘 u₂)
+    (hf₁ : IsBounded (range f₁)) (h2f₁ : HasCompactSupport f₁)
+    (hf₂ : IsBounded (range f₂)) (h2f₂ : HasCompactSupport f₂) :
+    ‖∫ x, adjointCarlesonSum (t u₁) g₁ x * conj (adjointCarlesonSum (t u₂) g₂ x)‖₊ ≤
+    C7_4_4 a n *
+    eLpNorm
+      ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₁ g₁) · |>.toReal) 2 volume *
+    eLpNorm
+      ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₂ g₂) · |>.toReal) 2 volume := by
+  sorry
+
+/-- Lemma 7.4.4. -/
+lemma correlation_separated_trees (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
+    (hf₁ : IsBounded (range f₁)) (h2f₁ : HasCompactSupport f₁)
+    (hf₂ : IsBounded (range f₂)) (h2f₂ : HasCompactSupport f₂) :
+    ‖∫ x, adjointCarlesonSum (t u₁) g₁ x * conj (adjointCarlesonSum (t u₂) g₂ x)‖₊ ≤
+    C7_4_4 a n *
+    eLpNorm
+      ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₁ g₁) · |>.toReal) 2 volume *
+    eLpNorm
+      ((𝓘 u₁ ∩ 𝓘 u₂ : Set X).indicator (adjointBoundaryOperator t u₂ g₂) · |>.toReal) 2 volume := by
+  sorry
+
+
+/-! ## Section 7.7 -/
+
+/-- The row-decomposition of a tree, defined in the proof of Lemma 7.7.1.
+The indexing is off-by-one compared to the blueprint. -/
+def rowDecomp (t : Forest X n) (j : ℕ) : Row X n := sorry
+
+/-- Part of Lemma 7.7.1 -/
+@[simp]
+lemma biUnion_rowDecomp : ⋃ j < 2 ^ n, t.rowDecomp j = (t : Set (𝔓 X)) := by
+  sorry
+
+/-- Part of Lemma 7.7.1 -/
+lemma pairwiseDisjoint_rowDecomp :
+    (Iio (2 ^ n)).PairwiseDisjoint (rowDecomp t · : ℕ → Set (𝔓 X)) := by
+  sorry
+
+@[simp] lemma rowDecomp_apply : t.rowDecomp j u = t u := by
+  sorry
+
+/-- The constant used in `row_bound`.
+Has value `2 ^ (156 * a ^ 3 - n / 2)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+irreducible_def C7_7_2_1 (a n : ℕ) : ℝ≥0 := 2 ^ (156 * (a : ℝ) ^ 3 - n / 2)
+
+/-- The constant used in `indicator_row_bound`.
+Has value `2 ^ (257 * a ^ 3 - n / 2)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+irreducible_def C7_7_2_2 (a n : ℕ) : ℝ≥0 := 2 ^ (257 * (a : ℝ) ^ 3 - n / 2)
+
+/-- Part of Lemma 7.7.2. -/
+lemma row_bound (hj : j < 2 ^ n) (hf : IsBounded (range f)) (h2f : HasCompactSupport f)
+    (h3f : AEStronglyMeasurable f) :
+    eLpNorm (∑ u ∈ {p | p ∈ rowDecomp t j}, adjointCarlesonSum (t u) f) 2 volume ≤
+    C7_7_2_1 a n * eLpNorm f 2 volume := by
+  sorry
+
+/-- Part of Lemma 7.7.2. -/
+lemma indicator_row_bound (hj : j < 2 ^ n) (hf : IsBounded (range f)) (h2f : HasCompactSupport f)
+    (h3f : AEStronglyMeasurable f) :
+    eLpNorm (∑ u ∈ {p | p ∈ rowDecomp t j}, F.indicator <| adjointCarlesonSum (t u) f) 2 volume ≤
+    C7_7_2_2 a n * dens₂ (⋃ u ∈ t, t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 volume := by
+  sorry
+
+/-- The constant used in `row_correlation`.
+Has value `2 ^ (862 * a ^ 3 - 3 * n)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+irreducible_def C7_7_3 (a n : ℕ) : ℝ≥0 := 2 ^ (862 * (a : ℝ) ^ 3 - 2 * n)
+
+/-- Lemma 7.7.3. -/
+lemma row_correlation (hjj' : j < j') (hj' : j' < 2 ^ n)
+    (hf₁ : IsBounded (range f₁)) (h2f₁ : HasCompactSupport f₁)
+    (hf₂ : IsBounded (range f₂)) (h2f₂ : HasCompactSupport f₂) :
+    ‖∫ x, (∑ u ∈ {p | p ∈ rowDecomp t j}, adjointCarlesonSum (t u) f₁ x) *
+    (∑ u ∈ {p | p ∈ rowDecomp t j'}, adjointCarlesonSum (t u) f₂ x)‖₊ ≤
+    C7_7_3 a n * eLpNorm f₁ 2 volume * eLpNorm f₂ 2 volume := by
+  sorry
+
+variable (t) in
+/-- The definition of `Eⱼ` defined above Lemma 7.7.4. -/
+def rowSupport (j : ℕ) : Set X := ⋃ (u ∈ rowDecomp t j) (p ∈ t u), E p
+
+/-- Lemma 7.7.4 -/
+lemma pairwiseDisjoint_rowSupport :
+    (Iio (2 ^ n)).PairwiseDisjoint (rowSupport t) := by
+  sorry
+
+end TileStructure.Forest
+
+/-! ## Proposition 2.0.4 -/
+
+/-- The constant used in `forest_operator`.
+Has value `2 ^ (432 * a ^ 3 - (q - 1) / q * n)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+irreducible_def C2_0_4 (a q : ℝ) (n : ℕ) : ℝ≥0 := 2 ^ (432 * a ^ 3 - (q - 1) / q * n)
+
+theorem forest_operator {n : ℕ} (𝔉 : Forest X n) {f g : X → ℂ}
+    (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hg : Measurable g)
+    (h2g : IsBounded (support g)) :
+    ‖∫ x, conj (g x) * ∑ u ∈ { p | p ∈ 𝔉 }, carlesonSum (𝔉 u) f x‖₊ ≤
+    C2_0_4 a q n * (dens₂ (X := X) (⋃ u ∈ 𝔉, 𝔉 u)) ^ (q⁻¹ - 2⁻¹) *
+    eLpNorm f 2 volume * eLpNorm g 2 volume := by
+  sorry