refactor carlesonOn definition to use Ks (task 403) (#492)

The result is closer to the blueprint and the code simpler across the board.

Author: JasperMS

Carleson/ForestOperator/PointwiseEstimate.lean

@@ -1053,13 +1053,13 @@ lemma pointwise_tree_estimate (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) (hx : x ∈
   set g := approxOnCube (𝓙 (t u)) f
   -- Convert the sum over `p` into a sum over `s`.
   unfold carlesonSum carlesonOn
-  rw [p_sum_eq_s_sum fun s x ↦ ∫ (y : X), cexp (I * (Q x y - Q x x)) * K x y *
-    («ψ» D (D ^ (-s) * dist x y)) * (fun y ↦ cexp (I * -𝒬 u y) * f y) y]
+  rw [p_sum_eq_s_sum fun s x ↦ ∫ (y : X), cexp (I * (Q x y - Q x x)) * Ks s x y *
+        (fun y ↦ cexp (I * -𝒬 u y) * f y) y]
   -- Next introduce an extra factor of `‖cexp (I * 𝒬 u x)‖ₑ`, i.e., 1. Then simplify.
   have : 1 = ‖cexp (I * 𝒬 u x)‖ₑ := by simp
   rw [← one_mul ‖_‖ₑ, this, ← enorm_mul, Finset.mul_sum]
-  have : ∑ i ∈ t.σ u x, cexp (I * 𝒬 u x) * ∫ (y : X), (cexp (I * (Q x y - Q x x)) * K x y *
-            («ψ» D (D ^ (-i) * dist x y)) * (cexp (I * -𝒬 u y) * f y)) =
+  have : ∑ i ∈ t.σ u x, cexp (I * 𝒬 u x) * ∫ (y : X), (cexp (I * (Q x y - Q x x)) * Ks i x y *
+            (cexp (I * -𝒬 u y) * f y)) =
           ∑ i ∈ t.σ u x, ∫ (y : X),
             (f y * ((exp (I * (- 𝒬 u y + Q x y + 𝒬 u x - Q x x)) - 1) * Ks i x y) +
             (f y - g y) * Ks i x y + g y * Ks i x y) := by

Carleson/Operators.lean

@@ -34,23 +34,19 @@ variable [TileStructure Q D κ S o] {p p' : 𝔓 X}
 /-- The operator `T_𝔭` defined in Proposition 2.0.2. -/
 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
+    fun x ↦ ∫ y, exp (I * (Q x y - Q x x)) * Ks (𝔰 p) x y * f y
 
 /- Deprecated for `AEStronglyMeasurable.carlesonOn`
 Used through `measurable_carlesonSum` in `Antichain.AntichainOperator` and `ForestOperator.Forests`
 with nontrivial rework in order to move from `Measurable` to `AEStronglyMeasurable`. -/
 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).mul ?_).mul ?_).stronglyMeasurable
+  refine ((Measurable.mul ?_ measurable_Ks).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
@@ -68,19 +64,13 @@ lemma _root_.MeasureTheory.AEStronglyMeasurable.carlesonOn {p : 𝔓 X} {f : X 
     (hf : AEStronglyMeasurable f) : AEStronglyMeasurable (carlesonOn p f) := by
   refine .indicator ?_ measurableSet_E
   refine .integral_prod_right'
-    (f := fun z ↦ exp (Complex.I * (Q z.1 z.2 - Q z.1 z.1)) * K z.1 z.2 *
-      ψ (D ^ (- 𝔰 p) * dist z.1 z.2) * f z.2) ?_
-  refine (((AEStronglyMeasurable.mul ?_ aestronglyMeasurable_K).mul ?_).mul ?_)
+    (f := fun z ↦ exp (Complex.I * (Q z.1 z.2 - Q z.1 z.1)) * Ks (𝔰 p) z.1 z.2 * f z.2) ?_
+  refine (AEStronglyMeasurable.mul ?_ aestronglyMeasurable_Ks).mul ?_
   · apply Measurable.aestronglyMeasurable
     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.aestronglyMeasurable
-    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 hf.comp_snd
 
 lemma _root_.MeasureTheory.AEStronglyMeasurable.carlesonSum {ℭ : Set (𝔓 X)}
@@ -359,11 +349,11 @@ theorem BoundedCompactSupport.adjointCarlesonSum {ℭ : Set (𝔓 X)}
 end MeasureTheory
 
 /-- `MKD` is short for "modulated kernel times dilated bump". -/
-private abbrev MKD (s : ℤ) x y := exp (I * (Q x y - Q x x)) * K x y * ψ (D ^ (-s) * dist x y)
+private abbrev MKD (s : ℤ) x y := exp (I * (Q x y - Q x x)) * Ks s x y (K := K)
 
 omit [TileStructure Q D κ S o] in
 private lemma norm_MKD_le_norm_Ks {s : ℤ} {x y : X} : ‖MKD s x y‖ ≤ ‖Ks s x y‖ := by
-  unfold MKD; rw [mul_assoc, ← Ks_def]
+  unfold MKD
   apply (norm_mul_le ..).trans
   apply le_of_eq
   rw [norm_exp_I_mul_sub_ofReal, one_mul]
@@ -405,7 +395,6 @@ lemma adjointCarleson_adjoint
             .indicator aestronglyMeasurable_const measurableSet_E
           exact this.comp_fst
       · unfold MKD
-        simp_rw [mul_assoc, ← Ks_def]
         refine .mul ?_ aestronglyMeasurable_Ks
         apply Measurable.aestronglyMeasurable
         have : Measurable fun (p : X × X) ↦ (p.1, p.1) :=
@@ -441,7 +430,7 @@ lemma adjointCarleson_adjoint
         _ = ∫ x in E p, conj (MKD (𝔰 p) x y) * g x := by congr; funext; rw [mul_comm]
         _ = _ := by
           unfold adjointCarleson MKD
-          congr; funext; rw [mul_assoc, ← Ks_def, map_mul, ← exp_conj, mul_comm (cexp _)]
+          congr; funext; rw [map_mul, ← exp_conj, mul_comm (cexp _)]
           congr; simp; ring
 
 /-- `adjointCarlesonSum` is the adjoint of `carlesonSum`. -/