various redefinitions, partly fix real_line file

Carleson.lean

@@ -1,10 +1,12 @@
-import Carleson.MetricCarleson
 import Carleson.CoverByBalls
 import Carleson.Defs
-import Carleson.DoublingMeasure
 import Carleson.DiscreteCarleson
+import Carleson.DoublingMeasure
+import Carleson.GridStructure
+import Carleson.MetricCarleson
 import Carleson.Proposition2
 import Carleson.Proposition3
+import Carleson.Psi
 import Carleson.Theorem1_1.Approximation
 import Carleson.Theorem1_1.Basic
 import Carleson.Theorem1_1.CarlesonOperatorReal

Carleson/Defs.lean

@@ -73,48 +73,57 @@ lemma fact_isCompact_ball (x : X) (r : ℝ) : Fact (IsBounded (ball x r)) :=
   ⟨isBounded_ball⟩
 attribute [local instance] fact_isCompact_ball
 
-/-- A class stating that continuous functions have distances associated to every ball. -/
+/-- A class stating that continuous functions have distances associated to every ball.
+We use a separate type to conveniently index these functions. -/
 class FunctionDistances (𝕜 : outParam Type*) (X : Type u)
     [NormedField 𝕜] [TopologicalSpace X] where
-  ι' : Type u
-  Θ : ι' → C(X, 𝕜)
-  out : ∀ (_x : X) (_r : ℝ), PseudoMetricSpace ι'
+  Θ : Type u
+  coeΘ : Θ → C(X, 𝕜)
+  metric : ∀ (_x : X) (_r : ℝ), PseudoMetricSpace Θ
 
-export FunctionDistances (ι' Θ)
+export FunctionDistances (Θ coeΘ)
+
+section FunctionDistances
+variable [FunctionDistances 𝕜 X]
+
+instance : Coe (Θ X) C(X, 𝕜) := ⟨coeΘ⟩
+instance : CoeFun (Θ X) (fun _ ↦ X → 𝕜) := ⟨fun f ↦ coeΘ f⟩
 
 set_option linter.unusedVariables false in
-def WithFunctionDistance (x : X) (r : ℝ) [FunctionDistances 𝕜 X] := ι' X
+def WithFunctionDistance (x : X) (r : ℝ) := Θ X
 
 variable {x : X} {r : ℝ}
 
-def toWithFunctionDistance [FunctionDistances 𝕜 X] : ι' X ≃ WithFunctionDistance x r :=
+def toWithFunctionDistance [FunctionDistances 𝕜 X] : Θ X ≃ WithFunctionDistance x r :=
   .refl _
 
--- instance : FunLike (WithFunctionDistance ι' x r) X 𝕜 := ContinuousMap.funLike
--- instance : ContinuousMapClass (WithFunctionDistance ι' x r) X 𝕜 :=
+-- instance : FunLike (WithFunctionDistance Θ x r) X 𝕜 := ContinuousMap.funLike
+-- instance : ContinuousMapClass (WithFunctionDistance Θ x r) X 𝕜 :=
 --   ContinuousMap.toContinuousMapClass
 
 instance [d : FunctionDistances 𝕜 X] : PseudoMetricSpace (WithFunctionDistance x r) :=
-  d.out x r
+  d.metric x r
+
+end FunctionDistances
 
-local notation3 "dist_{" x " ," r "}" => @dist (WithFunctionDistance x r) _
-local notation3 "ball_{" x " ," r "}" => @ball (WithFunctionDistance x r) _ in
+notation3 "dist_{" x " ," r "}" => @dist (WithFunctionDistance x r) _
+notation3 "ball_{" x " ," r "}" => @ball (WithFunctionDistance x r) _ in
 
 /-- A set `Θ` of (continuous) functions is compatible. `A` will usually be `2 ^ a`. -/
 class CompatibleFunctions (𝕜 : outParam Type*) (X : Type u) (A : outParam ℝ)
   [RCLike 𝕜] [PseudoMetricSpace X] extends FunctionDistances 𝕜 X where
-  eq_zero : ∃ o : X, ∀ f, Θ f o = 0
+  eq_zero : ∃ o : X, ∀ f : Θ, f o = 0
   /-- The distance is bounded below by the local oscillation. -/
-  localOscillation_le_cdist {x : X} {r : ℝ} {f g : ι'} :
-    localOscillation (ball x r) (Θ f) (Θ g) ≤ dist_{x, r} f g
+  localOscillation_le_cdist {x : X} {r : ℝ} {f g : Θ} :
+    localOscillation (ball x r) (coeΘ f) (coeΘ g) ≤ dist_{x, r} f g
   /-- The distance is monotone in the ball. -/
-  cdist_mono {x₁ x₂ : X} {r₁ r₂ : ℝ} {f g : ι'}
+  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
   /-- The distance of a ball with large radius is bounded above. -/
-  cdist_le {x₁ x₂ : X} {r : ℝ} {f g : ι'} (h : dist x₁ x₂ < 2 * r) :
+  cdist_le {x₁ x₂ : X} {r : ℝ} {f g : Θ} (h : dist x₁ x₂ < 2 * r) :
     dist_{x₂, 2 * r} f g ≤ A * dist_{x₁, r} f g
   /-- The distance of a ball with large radius is bounded below. -/
-  le_cdist {x₁ x₂ : X} {r : ℝ} {f g : ι'} (h1 : ball x₁ r ⊆ ball x₂ (A * r))
+  le_cdist {x₁ x₂ : X} {r : ℝ} {f g : Θ} (h1 : ball x₁ r ⊆ ball x₂ (A * r))
     /-(h2 : A * r ≤ Metric.diam (univ : Set X))-/ :
     2 * dist_{x₁, r} f g ≤ dist_{x₂, A * r} f g
   /-- The distance of a ball with large radius is bounded below. -/
@@ -127,11 +136,11 @@ variable (X) in
 /-- The point `o` in the blueprint -/
 def cancelPt [CompatibleFunctions 𝕜 X A] : X :=
   CompatibleFunctions.eq_zero (𝕜 := 𝕜) |>.choose
-def cancelPt_eq_zero [CompatibleFunctions 𝕜 X A] {f : ι' X} : Θ f (cancelPt X) = 0 :=
+def cancelPt_eq_zero [CompatibleFunctions 𝕜 X A] {f : Θ X} : f (cancelPt X) = 0 :=
   CompatibleFunctions.eq_zero (𝕜 := 𝕜) |>.choose_spec f
 
 lemma CompatibleFunctions.IsSeparable [CompatibleFunctions 𝕜 X A] :
-  IsSeparable (range (Θ (X := X))) :=
+  IsSeparable (range (coeΘ (X := X))) :=
   sorry
 
 set_option linter.unusedVariables false in
@@ -141,10 +150,10 @@ def iLipNorm {𝕜} [NormedField 𝕜] (ϕ : X → 𝕜) (x₀ : X) (R : ℝ) :
 
 variable (X) in
 /-- Θ is τ-cancellative. `τ` will usually be `1 / a` -/
-class IsCancellative (τ : ℝ) [CompatibleFunctions ℂ X A] : Prop where
+class IsCancellative (τ : ℝ) [CompatibleFunctions ℝ X A] : Prop where
   norm_integral_exp_le {x : X} {r : ℝ} {ϕ : X → ℂ} {K : ℝ≥0} (h1 : LipschitzWith K ϕ)
-    (h2 : tsupport ϕ ⊆ ball x r) {f g : ι' X} :
-    ‖∫ x in ball x r, exp (I * (Θ f x - Θ g x)) * ϕ x‖ ≤
+    (h2 : tsupport ϕ ⊆ ball x r) {f g : Θ X} :
+    ‖∫ x in ball x r, exp (I * (f x - g x)) * ϕ x‖ ≤
     A * volume.real (ball x r) * iLipNorm ϕ x r * (1 + dist_{x, r} f g) ^ (- τ)
 
 export IsCancellative (norm_integral_exp_le)
@@ -188,25 +197,26 @@ def NormBoundedBy {E F : Type*} [NormedAddCommGroup E] [NormedAddCommGroup F] (T
     Prop :=
   ∀ x, ‖T x‖ ≤ c * ‖x‖
 
+def HasStrongType {E E' α α' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E']
+    {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} (T : (α → E) → (α' → E'))
+    (μ : Measure α) (ν : Measure α') (p p' : ℝ≥0∞) (c : ℝ≥0) : Prop :=
+  ∀ f : α → E, Memℒp f p μ → AEStronglyMeasurable (T f) ν ∧ snorm (T f) p' ν ≤ c * snorm f p μ
+
 set_option linter.unusedVariables false in
 /-- The associated nontangential Calderon Zygmund operator -/
-def ANCZOperator (K : X → X → ℂ) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
+def ANCZOperator (K : X → X → ℂ) (f : X → ℂ) (x : X) : ℝ :=
   ⨆ (R₁ : ℝ) (R₂ : ℝ) (h1 : R₁ < R₂) (x' : X) (h2 : dist x x' ≤ R₁),
-  ‖∫ y in {y | dist x' y ∈ Ioo R₁ R₂}, K x' y * f y‖₊
-
-/-- The associated nontangential Calderon Zygmund operator, viewed as a map `L^p → L^p`.
-Todo: is `T_*f` indeed in L^p if `f` is? Needed at least for `p = 2`. -/
-def ANCZOperatorLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (K : X → X → ℂ) (f : Lp ℂ p (volume : Measure X)) :
-    Lp ℝ p (volume : Measure X) :=
-  Memℒp.toLp (ANCZOperator K (f : X → ℂ) · |>.toReal) sorry
+  ‖∫ y in {y | dist x' y ∈ Ioo R₁ R₂}, K x' y * f y‖₊ |>.toReal
 
--- /-- The generalized Carleson operator `T`, using real suprema -/
--- def Real.CarlesonOperator (K : X → X → ℂ) (Θ : Set C(X, ℂ)) (f : X → ℂ) (x : X) : ℝ :=
---   ⨆ (Q ∈ Θ) (R₁ : ℝ) (R₂ : ℝ) (_ : 0 < R₁) (_ : R₁ < R₂),
---   ‖∫ y in {y | dist x y ∈ Ioo R₁ R₂}, K x y * f y * Complex.exp (I * Q y)‖
+-- /-- The associated nontangential Calderon Zygmund operator, viewed as a map `L^p → L^p`.
+-- Todo: is `T_*f` indeed in L^p if `f` is? Needed at least for `p = 2`. -/
+-- def ANCZOperatorLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (K : X → X → ℂ)
+--     (f : Lp ℂ p (volume : Measure X)) : Lp ℝ p (volume : Measure X) :=
+--   Memℒp.toLp (ANCZOperator K (f : X → ℂ) · |>.toReal) sorry
 
-/-- The generalized Carleson operator `T`, ℝ≥0∞ version -/
+/-- The generalized Carleson operator `T`, taking values in `ℝ≥0∞`.
+Use `ENNReal.toReal` to get the corresponding real number. -/
 --TODO: remove the last two suprema?
-def CarlesonOperator (K : X → X → ℂ) (Θ : Set C(X, ℂ)) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
-  ⨆ (Q ∈ Θ) (R₁ : ℝ) (R₂ : ℝ) (_ : 0 < R₁) (_ : R₁ < R₂),
+def CarlesonOperator [FunctionDistances ℝ X] (K : X → X → ℂ) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
+  ⨆ (Q : Θ X) (R₁ : ℝ) (R₂ : ℝ) (_ : 0 < R₁) (_ : R₁ < R₂),
   ↑‖∫ y in {y | dist x y ∈ Ioo R₁ R₂}, K x y * f y * exp (I * Q y)‖₊

Carleson/DiscreteCarleson.lean

@@ -1,51 +1,43 @@
 import Carleson.GridStructure
+import Carleson.Psi
 -- import Carleson.Proposition2
 -- import Carleson.Proposition3
 
-open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators
+open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology
 open scoped ENNReal
 noncomputable section
 
-/- The constant used in proposition2_1 -/
-def C2_1 (a : ℝ) (q : ℝ) : ℝ := 2 ^ (440 * a ^ 3) / (q - 1) ^ 4
+/- The constant used in Proposition 2.0.2 -/
+def C2_2 (a : ℝ) (q : ℝ) : ℝ := 2 ^ (440 * a ^ 3) / (q - 1) ^ 4
 
-lemma C2_1_pos (a q : ℝ) : C2_1 a q > 0 := sorry
+lemma C2_2_pos (a q : ℝ) : C2_2 a q > 0 := sorry
 
-def D2_1 (A : ℝ) (τ q : ℝ) (C : ℝ) : ℝ := sorry
+def D2_2 (a : ℝ) : ℝ := 2 ^ (100 * a ^ 2)
 
-lemma D2_1_pos (A : ℝ) (τ q : ℝ) (C : ℝ) : D2_1 A τ q C > 0 := sorry
+lemma D2_2_pos (a : ℝ) : D2_2 a > 0 := sorry
 
-def κ2_1 (A : ℝ) (τ q : ℝ) (C : ℝ) : ℝ := sorry
+def κ2_2 (A : ℝ) (τ q : ℝ) (C : ℝ) : ℝ := sorry
 
-lemma κ2_1_pos (A : ℝ) (τ q : ℝ) (C : ℝ) : κ2_1 A τ q C > 0 := sorry
+lemma κ2_2_pos (A : ℝ) (τ q : ℝ) (C : ℝ) : κ2_2 A τ q C > 0 := sorry
 
--- this should be `10 * D` or something
-def Cψ2_1 (A : ℝ) (τ q : ℝ) (C : ℝ) : ℝ≥0 := sorry
-
-lemma Cψ2_1_pos (A : ℝ) (τ : ℝ) (C : ℝ) : Cψ2_1 A τ C > 0 := sorry
-
-/-
-variable {X : Type*} {A : ℝ} [MetricSpace X] [DoublingMeasure X A] [Inhabited X]
+variable {X : Type*} {a : ℝ} [MetricSpace X] [DoublingMeasure X (2 ^ a)] [Inhabited X]
 variable {τ q q' D κ : ℝ} {C₀ C : ℝ}
-variable {Θ : Set C(X, ℂ)} [IsCompatible Θ] [IsCancellative τ Θ] [TileStructure Θ D κ C₀]
-variable {F G : Set X} {σ σ' : X → ℤ} {Q' : X → C(X, ℂ)} /- Q-tilde in the pdf -/
+variable [CompatibleFunctions ℝ X (2 ^ a)] [IsCancellative X τ]
+variable {Q : X → Θ X} {S : ℤ} {o : X} [TileStructure Q D κ C S o]
+variable {F G : Set X} {σ₁ σ₂ : X → ℤ} {Q : X → Θ X}
 variable (K : X → X → ℂ) [IsCZKernel τ K]
-variable {ψ : ℝ → ℝ}
 
 -- todo: add some conditions that σ and other functions have finite range?
 -- todo: fix statement
 theorem discrete_carleson
-    (hA : 1 < A) (hτ : τ ∈ Ioo 0 1) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjExponent q')
-    (hC₀ : 0 < C₀) (hC : C2_1 A τ q C₀ < C) (hD : D2_1 A τ q C₀ < D)
-    (hκ : κ ∈ Ioo 0 (κ2_1 A τ q C₀))
+    (hA : 4 ≤ a) (hτ : τ ∈ Ioo 0 1) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjExponent q')
+    -- (hC₀ : 0 < C₀) (hC : C2_2 A τ q C₀ < C) (hD : D2_2 A τ q C₀ < D)
+    (hκ : κ ∈ Ioo 0 (κ2_2 (2 ^ a) τ q C₀))
     (hF : MeasurableSet F) (hG : MeasurableSet G)
-    (h2F : volume F ∈ Ioo 0 ∞) (h2G : volume G ∈ Ioo 0 ∞)
-    (Q'_mem : ∀ x, Q' x ∈ Θ) (m_Q' : Measurable Q')
-    (m_σ : Measurable σ) (m_σ' : Measurable σ')
-    (hT : NormBoundedBy (ANCZOperatorLp 2 K) 1)
-    (hψ : LipschitzWith (Cψ2_1 A τ q C₀) ψ)
-    (h2ψ : support ψ ⊆ Icc (4 * D)⁻¹ 2⁻¹) (h3ψ : ∀ x > 0, ∑ᶠ s : ℤ, ψ (D ^ s * x) = 1)
+    (h2F : IsBounded F) (h2G : IsBounded G)
+    (m_σ₁ : Measurable σ₁) (m_σ₂ : Measurable σ₂)
+    (hT : HasStrongType (ANCZOperator K) volume volume 2 2 1)
     :
-    ∃ G', volume G' ≤ volume G / 4 ∧ ‖∫ x in G \ G', ∑' p, T K Q' σ σ' ψ p F 1 x‖₊ ≤
-    C * (volume.real G) ^ (1 / q') * (volume.real F) ^ (1 / q) := by sorry
--/
+    ∃ G', 2 * volume G' ≤ volume G ∧ ∀ f : X → ℂ, (∀ x, ‖f x‖ ≤ F.indicator 1 x) →
+    ‖∫ x in G \ G', ∑' p, T K σ₁ σ₂ (ψ (D2_2 a)) p F 1 x‖₊ ≤
+    C2_2 a q * (volume.real G) ^ (1 / q') * (volume.real F) ^ (1 / q) := by sorry

Carleson/GridStructure.lean

@@ -4,7 +4,7 @@ open Set MeasureTheory Metric Function Complex
 open scoped ENNReal
 noncomputable section
 
-variable {𝕜 : Type*} {A : ℝ} [_root_.RCLike 𝕜]
+variable {𝕜 : Type*} [_root_.RCLike 𝕜]
 variable {X : Type*} {A : ℝ} [PseudoMetricSpace X] [DoublingMeasure X A]
 
 variable (X) in
@@ -70,8 +70,8 @@ class TileStructureData.{u} [FunctionDistances 𝕜 X]
   fintype_𝔓 : Fintype 𝔓
   protected 𝓘 : 𝔓 → ι
   surjective_𝓘 : Surjective 𝓘
-  Ω : 𝔓 → Set (ι' X)
-  𝒬 : 𝔓 → ι' X
+  Ω : 𝔓 → Set (Θ X)
+  𝒬 : 𝔓 → Θ X
 
 export TileStructureData (Ω 𝒬)
 
@@ -91,55 +91,55 @@ notation3 "dist_(" D "," 𝔭 ")" => @dist (WithFunctionDistance (𝔠 𝔭) (D
 notation3 "ball_(" D "," 𝔭 ")" => @ball (WithFunctionDistance (𝔠 𝔭) (D ^ 𝔰 𝔭 / 4)) _
 
 /-- A tile structure. -/
-class TileStructure [FunctionDistances ℂ X] (Q : outParam (X → C(X, ℂ)))
+class TileStructure [FunctionDistances ℝ X] (Q : outParam (X → Θ X))
     (D κ C : outParam ℝ) (S : outParam ℤ) (o : outParam X)
     extends TileStructureData D κ C S o where
-  biUnion_Ω {i} : range Q ⊆ Θ '' ⋃ p ∈ 𝓘 ⁻¹' {i}, Ω p
+  biUnion_Ω {i} : range Q ⊆ ⋃ p ∈ 𝓘 ⁻¹' {i}, Ω p
   disjoint_Ω {p p'} (h : p ≠ p') (hp : 𝓘 p = 𝓘 p') : Disjoint (Ω p) (Ω p')
   relative_fundamental_dyadic {p p'} (h : 𝓓 (𝓘 p) ⊆ 𝓓 (𝓘 p')) : Disjoint (Ω p) (Ω p') ∨ Ω p' ⊆ Ω p
   cdist_subset {p} : ball_(D, p) (𝒬 p) 5⁻¹ ⊆ Ω p
   subset_cdist {p} : Ω p ⊆ ball_(D, p) (𝒬 p) 1
 
 export TileStructure (biUnion_Ω disjoint_Ω relative_fundamental_dyadic cdist_subset subset_cdist)
 
-variable {Q : X → C(X, ℂ)} [FunctionDistances ℂ X] [TileStructure Q D κ C S o]
+variable [FunctionDistances ℝ X] {Q : X → Θ X} [TileStructure Q D κ C S o]
 
-/- The set `E` defined in Proposition 2.1. -/
-def E (σ σ' : X → ℤ) (p : 𝔓 X) : Set X :=
-  { x ∈ 𝓓 (𝓘 p) | Q x ∈ Θ '' Ω p ∧ 𝔰 p ∈ Icc (σ x) (σ' x) }
+/- The set `E` defined in Proposition 2.0.2. -/
+def E (σ₁ σ₂ : X → ℤ) (p : 𝔓 X) : Set X :=
+  { x ∈ 𝓓 (𝓘 p) | Q x ∈ Ω p ∧ 𝔰 p ∈ Icc (σ₁ x) (σ₂ x) }
 
 section T
 
-variable (K : X → X → ℂ) (σ σ' : X → ℤ) (ψ : ℝ → ℝ) (p : 𝔓 X) (F : Set X)
+variable (K : X → X → ℂ) (σ₁ σ₂ : X → ℤ) (ψ : ℝ → ℝ) (p : 𝔓 X) (F : Set X)
 
-/- The operator `T` defined in Proposition 2.1, considered on the set `F`.
+/- The operator `T` defined in Proposition 2.0.2, considered on the set `F`.
 It is the map `T ∘ (1_F * ·) : f ↦ T (1_F * f)`, also denoted `T1_F`
-The operator `T` in Proposition 2.1 is therefore `applied to `(F := Set.univ)`. -/
+The operator `T` in Proposition 2.0.2 is therefore `applied to `(F := Set.univ)`. -/
 def T (f : X → ℂ) : X → ℂ :=
-  indicator (E σ σ' p)
+  indicator (E σ₁ σ₂ p)
     fun x ↦ ∫ y, exp (Q x x - Q x y) * K x y * ψ (D ^ (- 𝔰 p) * dist x y) * F.indicator f y
 
-lemma Memℒp_T {f : X → ℂ} {q : ℝ≥0∞} (hf : Memℒp f q) : Memℒp (T K σ σ' ψ p F f) q :=
+lemma Memℒp_T {f : X → ℂ} {q : ℝ≥0∞} (hf : Memℒp f q) : Memℒp (T K σ₁ σ₂ ψ p F f) q :=
   by sorry
 
 /- The operator `T`, defined on `L^2` maps. -/
 def T₂ (f : X →₂[volume] ℂ) : X →₂[volume] ℂ :=
-  Memℒp.toLp (T K σ σ' ψ p F f) <| Memℒp_T K σ σ' ψ p F <| Lp.memℒp f
+  Memℒp.toLp (T K σ₁ σ₂ ψ p F f) <| Memℒp_T K σ₁ σ₂ ψ p F <| Lp.memℒp f
 
 /- The operator `T`, defined on `L^2` maps as a continuous linear map. -/
 def TL : (X →₂[volume] ℂ) →L[ℂ] (X →₂[volume] ℂ) where
-    toFun := T₂ K σ σ' ψ p F
+    toFun := T₂ K σ₁ σ₂ ψ p F
     map_add' := sorry
     map_smul' := sorry
     cont := by sorry
 
 end T
 
 variable (X) in
-def TileLike : Type _ := Set X × OrderDual (Set (ι' X))
+def TileLike : Type _ := Set X × OrderDual (Set (Θ X))
 
 def TileLike.fst (x : TileLike X) : Set X := x.1
-def TileLike.snd (x : TileLike X) : Set (ι' X) := x.2
+def TileLike.snd (x : TileLike X) : Set (Θ X) := x.2
 instance : PartialOrder (TileLike X) := by dsimp [TileLike]; infer_instance
 example (x y : TileLike X) : x ≤ y ↔ x.fst ⊆ y.fst ∧ y.snd ⊆ x.snd := by rfl
 
@@ -150,9 +150,9 @@ lemma toTileLike_injective : Injective (fun p : 𝔓 X ↦ toTileLike p) := sorr
 instance : PartialOrder (𝔓 X) := PartialOrder.lift toTileLike toTileLike_injective
 
 def smul (a : ℝ) (p : 𝔓 X) : TileLike X :=
-  sorry --(𝓓 (𝓘 p), localOscillationBall (𝓓 (𝓘 p)) (Θ (𝒬 p)) a)
+  (𝓓 (𝓘 p), ball_(D, p) (𝒬 p) a)
 
-def TileLike.toTile (t : TileLike X) : Set (X × ι' X) :=
+def TileLike.toTile (t : TileLike X) : Set (X × Θ X) :=
   t.fst ×ˢ t.snd
 
 lemma isAntichain_iff_disjoint (𝔄 : Set (𝔓 X)) :
@@ -163,10 +163,10 @@ lemma isAntichain_iff_disjoint (𝔄 : Set (𝔓 X)) :
 def convexShadow (𝔓' : Set (𝔓 X)) : Set (ι X) :=
   { i | ∃ p p' : 𝔓 X, p ∈ 𝔓' ∧ p' ∈ 𝔓' ∧ (𝓓 (𝓘 p) : Set X) ⊆ 𝓓 i ∧ 𝓓 i ⊆ 𝓓 (𝓘 p') }
 
-def EBar (G : Set X) (Q : X → ι' X) (t : TileLike X) : Set X :=
+def EBar (G : Set X) (Q : X → Θ X) (t : TileLike X) : Set X :=
   { x ∈ t.fst ∩ G | Q x ∈ t.snd }
 
-def density (G : Set X) (Q : X → ι' X) (𝔓' : Set (𝔓 X)) : ℝ :=
+def density (G : Set X) (Q : X → Θ X) (𝔓' : Set (𝔓 X)) : ℝ :=
   ⨆ (p ∈ 𝔓') (l ≥ (2 : ℝ)), l ^ (-2 * Real.log A) *
   ⨆ (p' : 𝔓 X) (_h : 𝓘 p' ∈ convexShadow 𝔓') (_h2 : smul l p ≤ smul l p'),
   volume.real (EBar G Q (smul l p')) / volume.real (EBar G Q (toTileLike p))

Carleson/MetricCarleson.lean

@@ -32,7 +32,6 @@ section -- todo: old code
 variable {X : Type*} {a : ℝ} [MetricSpace X]
   [DoublingMeasure X (2 ^ a)] [Inhabited X]
 variable {τ q q' : ℝ} {C : ℝ}
-variable {Θ : Set C(X, ℂ)}
 variable {F G : Set X}
 variable (K : X → X → ℂ)
 
@@ -130,16 +129,17 @@ segment. -/
 (section 2). -/
 
 /- Theorem 1.2, written using constant C1_2 -/
-theorem metric_carleson [CompatibleFunctions ℂ X (2 ^ a)]
+theorem metric_carleson [CompatibleFunctions ℝ X (2 ^ a)]
   [IsCancellative X (2 ^ a)] [IsCZKernel a K]
     (ha : 4 ≤ a) (hq : q ∈ Ioc 1 2) (hqq' : q.IsConjExponent q')
     (hF : MeasurableSet F) (hG : MeasurableSet G)
     -- (h2F : volume F ∈ Ioo 0 ∞) (h2G : volume G ∈ Ioo 0 ∞)
     -- (hT : NormBoundedBy (ANCZOperatorLp 2 K) (2 ^ a ^ 3))
-    (hT : ∀ (g : X → ℂ) (hg : Memℒp g ∞) (h2g : volume (support g) < ∞) (h3g : Memℒp g 2 volume),
-      snorm (ANCZOperatorLp 2 K h3g.toLp) 2 volume ≤ 2 ^ a ^ (3 : ℕ) * snorm g 2 volume)
+    (hT : ∀ (g : X → ℂ) (hg : Memℒp g ∞ volume) (h2g : volume (support g) < ∞)
+      (h3g : Memℒp g 2 volume),
+      snorm (ANCZOperator K g) 2 volume ≤ 2 ^ a ^ (3 : ℕ) * snorm g 2 volume)
     (f : X → ℂ) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
-    ∫⁻ x in G, CarlesonOperator K Θ f x ≤
+    ∫⁻ x in G, CarlesonOperator K f x ≤
     ENNReal.ofReal (C1_2 a q) * (volume G) ^ q'⁻¹ * (volume F) ^ q⁻¹ := by
   sorry
 

Carleson/Proposition2.lean

@@ -3,7 +3,7 @@ import Carleson.GridStructure
 open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators
 open scoped ENNReal
 noncomputable section
-
+/-
 def C2_2 (A : ℝ) (τ q : ℝ) (C : ℝ) : ℝ := sorry
 
 lemma C2_2_pos (A : ℝ) (τ q : ℝ) (C : ℝ) : C2_2 A τ q C > 0 := sorry
@@ -24,7 +24,7 @@ lemma κ2_2_pos (A : ℝ) (τ q : ℝ) (C : ℝ) : κ2_2 A τ q C > 0 := sorry
 def Cψ2_2 (A : ℝ) (τ q : ℝ) (C : ℝ) : ℝ≥0 := sorry
 
 lemma Cψ2_2_pos (A : ℝ) (τ : ℝ) (C : ℝ) : Cψ2_2 A τ C > 0 := sorry
-/-
+
 variable {X : Type*} {A : ℝ} [MetricSpace X] [DoublingMeasure X A] [Inhabited X]
 variable {τ q D κ ε : ℝ} {C₀ C t : ℝ}
 variable {Θ : Set C(X, ℂ)} [IsCompatible Θ] [IsCancellative τ Θ] [TileStructure Θ D κ C₀]