diff --git a/Carleson/AntichainOperator.lean b/Carleson/AntichainOperator.lean
index d37c7438..c7608b38 100644
--- a/Carleson/AntichainOperator.lean
+++ b/Carleson/AntichainOperator.lean
@@ -1,22 +1,21 @@
 import Carleson.GridStructure
 
-variable {𝕜 : Type*} [_root_.RCLike 𝕜]
-variable {X : Type*} {A : ℝ} [PseudoMetricSpace X] [DoublingMeasure X A]
-variable {D κ C : ℝ} {S : ℤ} {o : X}
-variable [FunctionDistances ℝ X] {Q : X → Θ X} [TileStructure Q D κ C S o]
+open scoped ShortVariables
+variable {X : Type*} {a q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X}
+  [ProofData a q K σ₁ σ₂ F G] [TileStructure Q D κ S o]
 
 open scoped GridStructure
 open Set
 
 -- Lemma 6.1.1
 lemma E_disjoint (σ σ' : X → ℤ) {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (·≤·) 𝔄) {p p' : 𝔓 X}
-    (hp : p ∈ 𝔄) (hp' : p' ∈ 𝔄) (hE : (E σ σ' p ∩ E σ σ' p').Nonempty) : p = p' := by
+    (hp : p ∈ 𝔄) (hp' : p' ∈ 𝔄) (hE : (E p ∩ E p').Nonempty) : p = p' := by
   set x := hE.some
   have hx := hE.some_mem
   simp only [E, mem_inter_iff, mem_setOf_eq] at hx
   wlog h𝔰 : 𝔰 p ≤ 𝔰 p'
-  · have hE' : (E σ σ' p' ∩ E σ σ' p).Nonempty := by simp only [inter_comm, hE]
-    exact eq_comm.mp (this (𝕜 := 𝕜) σ σ' h𝔄 hp' hp hE' hE'.some_mem (le_of_lt (not_le.mp h𝔰)))
+  · have hE' : (E p' ∩ E p).Nonempty := by simp only [inter_comm, hE]
+    exact eq_comm.mp (this σ σ' h𝔄 hp' hp hE' hE'.some_mem (le_of_lt (not_le.mp h𝔰)))
   obtain ⟨⟨hx𝓓p, hxΩp, _⟩ , hx𝓓p', hxΩp', _⟩ := hx
   have h𝓓 : 𝓓 (𝓘 p) ⊆ 𝓓 (𝓘 p') :=
     (or_iff_left (not_disjoint_iff.mpr ⟨x, hx𝓓p, hx𝓓p'⟩)).mp (fundamental_dyadic h𝔰)
diff --git a/Carleson/Defs.lean b/Carleson/Defs.lean
index 9accbd1b..578fd846 100644
--- a/Carleson/Defs.lean
+++ b/Carleson/Defs.lean
@@ -10,6 +10,7 @@ noncomputable section
 These are mostly the definitions used to state the metric Carleson theorem.
 We should move them to separate files once we start proving things about them. -/
 
+section DoublingMeasure
 universe u
 variable {𝕜 X : Type*} {A : ℝ} [_root_.RCLike 𝕜] [PseudoMetricSpace X] [DoublingMeasure X A]
 
@@ -139,6 +140,7 @@ def cancelPt [CompatibleFunctions 𝕜 X A] : X :=
 def cancelPt_eq_zero [CompatibleFunctions 𝕜 X A] {f : Θ X} : f (cancelPt X) = 0 :=
   CompatibleFunctions.eq_zero (𝕜 := 𝕜) |>.choose_spec f
 
+-- not sure if needed
 lemma CompatibleFunctions.IsSeparable [CompatibleFunctions 𝕜 X A] :
   IsSeparable (range (coeΘ (X := X))) :=
   sorry
@@ -195,25 +197,30 @@ Reference: https://arxiv.org/abs/math/9910039
 Lemma 3.6 - Lemma 3.9
 -/
 
-/-- This is usually the value of the argument `A` in `DoublingMeasure`
-and `CompatibleFunctions` -/
-@[simp] abbrev defaultA (a : ℝ) : ℝ := 2 ^ a
-@[simp] def defaultD (a : ℝ) : ℝ := 2 ^ (100 * a ^ 2)
-@[simp] def defaultκ (a : ℝ) : ℝ := 2 ^ (- 10 * a)
-@[simp] def defaultZ (a : ℝ) : ℝ := 2 ^ (12 * a)
-
 /-- This can be useful to say that `‖T‖ ≤ c`. -/
 def NormBoundedBy {E F : Type*} [NormedAddCommGroup E] [NormedAddCommGroup F] (T : E → F) (c : ℝ) :
     Prop :=
   ∀ x, ‖T x‖ ≤ c * ‖x‖
 
+/-- An operator has strong type (p, q) if it is bounded as an operator on L^p → L^q.
+We write `HasStrongType T μ ν p p' c` to say that `T` has strong type (p, q) w.r.t. measures `μ`, `ν` and constant `c`.  -/
 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 μ
 
+-- todo: define `HasWeakType`
+
+/-- A weaker version of `HasStrongType`, where we add additional assumptions on the function `f`.
+Note(F): I'm not sure if this is an equivalent characterization of having weak type (p, q) -/
+def HasBoundedStrongType {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 μ → snorm f ∞ μ < ∞ → μ (support f) < ∞ →
+  AEStronglyMeasurable (T f) ν ∧ snorm (T f) p' ν ≤ c * snorm f p μ
+
 set_option linter.unusedVariables false in
-/-- The associated nontangential Calderon Zygmund operator -/
+/-- The associated nontangential Calderon Zygmund operator `T_*` -/
 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‖₊ |>.toReal
@@ -230,3 +237,74 @@ Use `ENNReal.toReal` to get the corresponding real number. -/
 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)‖₊
+
+
+end DoublingMeasure
+
+
+/-- This is usually the value of the argument `A` in `DoublingMeasure`
+and `CompatibleFunctions` -/
+@[simp] abbrev defaultA (a : ℝ) : ℝ := 2 ^ a
+@[simp] def defaultD (a : ℝ) : ℝ := 2 ^ (100 * a ^ 2)
+@[simp] def defaultκ (a : ℝ) : ℝ := 2 ^ (- 10 * a)
+@[simp] def defaultZ (a : ℝ) : ℝ := 2 ^ (12 * a)
+
+/- A constant used on the boundedness of `T_*`. We generally assume
+`HasBoundedStrongType (ANCZOperator K) volume volume 2 2 (C_Ts a)`
+throughout this formalization. -/
+def C_Ts (a : ℝ) : ℝ≥0 := 2 ^ a ^ 3
+
+/-- Data common through most of chapters 2-9. -/
+class PreProofData {X : Type*} (a q : outParam ℝ) (K : outParam (X → X → ℂ))
+  (σ₁ σ₂ : outParam (X → ℤ)) (F G : outParam (Set X)) where
+  m : PseudoMetricSpace X
+  d : DoublingMeasure X (2 ^ a)
+  ha : 4 ≤ a
+  cf : CompatibleFunctions ℝ X (2 ^ a)
+  c : IsCancellative X a⁻¹
+  hasBoundedStrongType_T : HasBoundedStrongType (ANCZOperator K) volume volume 2 2 (C_Ts a)
+  hF : MeasurableSet F
+  hG : MeasurableSet G
+  m_σ₁ : Measurable σ₁
+  m_σ₂ : Measurable σ₂
+  f_σ₁ : Finite (range σ₁)
+  f_σ₂ : Finite (range σ₂)
+  hσ₁₂ : σ₁ ≤ σ₂
+  Q : SimpleFunc X (Θ X)
+  hq : q ∈ Ioc 1 2
+
+
+export PreProofData (ha hasBoundedStrongType_T hF hG m_σ₁ m_σ₂ f_σ₁ f_σ₂ Q)
+attribute [instance] PreProofData.m PreProofData.d PreProofData.cf PreProofData.c
+
+section ProofData
+
+variable {X : Type*} {a q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X}
+
+variable (X) in
+def S_spec [PreProofData a q K σ₁ σ₂ F G] : ∃ n : ℕ, ∀ x, -n ≤ σ₁ x ∧ σ₂ x ≤ n := sorry
+
+variable (X) in
+open Classical in
+def S [PreProofData a q K σ₁ σ₂ F G] : ℤ := Nat.find (S_spec X)
+
+lemma range_σ₁_subset [PreProofData a q K σ₁ σ₂ F G] : range σ₁ ⊆ Icc (- S X) (S X) := sorry
+
+lemma range_σ₂_subset [PreProofData a q K σ₁ σ₂ F G] : range σ₂ ⊆ Icc (- S X) (S X) := sorry
+
+end ProofData
+
+class ProofData {X : Type*} (a q : outParam ℝ) (K : outParam (X → X → ℂ))
+  (σ₁ σ₂ : outParam (X → ℤ)) (F G : outParam (Set X)) extends PreProofData a q K σ₁ σ₂ F G where
+  F_subset : F ⊆ ball (cancelPt X) (defaultD a ^ S X)
+  G_subset : G ⊆ ball (cancelPt X) (defaultD a ^ S X)
+
+namespace ShortVariables
+
+set_option hygiene false
+scoped notation "D" => defaultD a
+scoped notation "κ" => defaultκ a
+scoped notation "o" => cancelPt X
+scoped notation "S" => S X
+
+end ShortVariables
diff --git a/Carleson/DiscreteCarleson.lean b/Carleson/DiscreteCarleson.lean
index 8d80f119..36e6ce9d 100644
--- a/Carleson/DiscreteCarleson.lean
+++ b/Carleson/DiscreteCarleson.lean
@@ -12,32 +12,17 @@ def C2_2 (a : ℝ) (q : ℝ) : ℝ := 2 ^ (440 * a ^ 3) / (q - 1) ^ 4
 
 lemma C2_2_pos (a q : ℝ) : C2_2 a q > 0 := sorry
 
-def D2_2 (a : ℝ) : ℝ := 2 ^ (100 * a ^ 2)
+open scoped ShortVariables
+variable {X : Type*} {a q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X}
 
-lemma D2_2_pos (a : ℝ) : D2_2 a > 0 := sorry
+-- variable {X : Type*} {a : ℝ} [MetricSpace X] [DoublingMeasure X (2 ^ a)] [Inhabited X]
+-- variable {τ q q' D κ : ℝ} {C₀ C : ℝ}
+-- variable [CompatibleFunctions ℝ X (2 ^ a)] [IsCancellative X τ]
+-- variable {Q : X → Θ X} {S : ℤ} {o : X} [TileStructure Q D κ S o]
+-- variable {F G : Set X} {σ₁ σ₂ : X → ℤ} {Q : X → Θ X}
+-- variable (K : X → X → ℂ) [IsCZKernel τ K]
 
-def κ2_2 (A : ℝ) (τ q : ℝ) (C : ℝ) : ℝ := sorry
-
-lemma κ2_2_pos (A : ℝ) (τ q : ℝ) (C : ℝ) : κ2_2 A τ q C > 0 := sorry
-
-variable {X : Type*} {a : ℝ} [MetricSpace X] [DoublingMeasure X (2 ^ a)] [Inhabited X]
-variable {τ q q' D κ : ℝ} {C₀ C : ℝ}
-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]
-
--- todo: add some conditions that σ and other functions have finite range?
--- todo: fix statement
-theorem discrete_carleson
-    (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 : IsBounded F) (h2G : IsBounded G)
-    (m_σ₁ : Measurable σ₁) (m_σ₂ : Measurable σ₂)
-    (hT : HasStrongType (ANCZOperator K) volume volume 2 2 1)
-    :
+theorem discrete_carleson [ProofData a q K σ₁ σ₂ F G] [TileStructure Q D κ S o] :
     ∃ 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
+    ‖∫ x in G \ G', ∑' p, T p f x‖₊ ≤
+    C2_2 a q * (volume.real G) ^ (1 - 1 / q) * (volume.real F) ^ (1 / q) := by sorry
diff --git a/Carleson/GridStructure.lean b/Carleson/GridStructure.lean
index 41200203..fedcf8bf 100644
--- a/Carleson/GridStructure.lean
+++ b/Carleson/GridStructure.lean
@@ -1,9 +1,11 @@
 import Carleson.Defs
+import Carleson.Psi
 
-open Set MeasureTheory Metric Function Complex
-open scoped NNReal ENNReal
+open Set MeasureTheory Metric Function Complex Bornology
+open scoped NNReal ENNReal ComplexConjugate
 noncomputable section
 
+section DoublingMeasure
 variable {𝕜 : Type*} [_root_.RCLike 𝕜]
 variable {X : Type*} {A : ℝ} [PseudoMetricSpace X] [DoublingMeasure X A]
 
@@ -12,7 +14,8 @@ variable (X) in
 I expect we prefer `𝓓 : ι → Set X` over `𝓓 : Set (Set X)`
 Note: the `s` in this paper is `-s` of Christ's paper.
 -/
-class GridStructure (D κ C : outParam ℝ) (S : outParam ℤ) (o : outParam X) where
+class GridStructure
+    (D κ : outParam ℝ) (S : outParam ℤ) (o : outParam X) where
   /-- indexing set for a grid structure -/
   ι : Type*
   fintype_ι : Fintype ι
@@ -29,7 +32,7 @@ class GridStructure (D κ C : outParam ℝ) (S : outParam ℤ) (o : outParam X)
   ball_subset_𝓓 {i} : ball (c i) (D ^ s i / 4) ⊆ 𝓓 i
   𝓓_subset_ball {i} : 𝓓 i ⊆ ball (c i) (4 * D ^ s i)
   small_boundary {i} {t : ℝ} (ht : D ^ (- S - s i) ≤ t) :
-    volume.real { x ∈ 𝓓 i | infDist x (𝓓 i)ᶜ ≤ t * D ^ s i } ≤ C * t ^ κ * volume.real (𝓓 i)
+    volume.real { x ∈ 𝓓 i | infDist x (𝓓 i)ᶜ ≤ t * D ^ s i } ≤ D * t ^ κ * volume.real (𝓓 i)
 
 export GridStructure (range_s_subset 𝓓_subset_biUnion
   fundamental_dyadic ball_subset_biUnion ball_subset_𝓓 𝓓_subset_ball small_boundary)
@@ -38,7 +41,7 @@ variable {D κ C : ℝ} {S : ℤ} {o : X}
 
 section GridStructure
 
-variable [GridStructure X D κ C S o]
+variable [GridStructure X D κ S o]
 
 variable (X) in
 def ι : Type* := GridStructure.ι X A
@@ -56,7 +59,7 @@ def grid_existence {σ₁ σ₂ : X → ℤ} (hσ : σ₁ ≤ σ₂)
     {F G : Set X} (hF : Measurable F) (hG : Measurable G)
     (h2F : F ⊆ ball o (D ^ S)) (h2G : G ⊆ ball o (D ^ S))
     (hσ₁S : range σ₁ ⊆ Icc (-S) S) (hσ₂S : range σ₂ ⊆ Icc (-S) S) :
-    GridStructure X D κ C S o :=
+    GridStructure X D κ S o :=
   sorry
 
 -- instance homogeneousMeasurableSpace [Inhabited X] : MeasurableSpace C(X, ℝ) :=
@@ -69,7 +72,7 @@ def grid_existence {σ₁ σ₂ : X → ℤ} (hσ : σ₁ ≤ σ₂)
 This is mostly separated out so that we can nicely define the notation `d_𝔭`.
 Note: compose `𝓘` with `𝓓` to get the `𝓘` of the paper. -/
 class TileStructureData.{u} [FunctionDistances 𝕜 X]
-  (D κ C : outParam ℝ) (S : outParam ℤ) (o : outParam X) extends GridStructure X D κ C S o where
+  (D κ : outParam ℝ) (S : outParam ℤ) (o : outParam X) extends GridStructure X D κ S o where
   protected 𝔓 : Type u
   fintype_𝔓 : Fintype 𝔓
   protected 𝓘 : 𝔓 → ι
@@ -80,7 +83,7 @@ class TileStructureData.{u} [FunctionDistances 𝕜 X]
 export TileStructureData (Ω 𝒬)
 
 section
-variable {Q : X → C(X, ℂ)} [FunctionDistances 𝕜 X] [TileStructureData D κ C S o]
+variable {Q : X → C(X, ℂ)} [FunctionDistances 𝕜 X] [TileStructureData D κ S o]
 
 variable (X) in
 def 𝔓 := TileStructureData.𝔓 𝕜 X A
@@ -96,8 +99,8 @@ notation3 "ball_(" D "," 𝔭 ")" => @ball (WithFunctionDistance (𝔠 𝔭) (D
 
 /-- A tile structure. -/
 class TileStructure [FunctionDistances ℝ X] (Q : outParam (X → Θ X))
-    (D κ C : outParam ℝ) (S : outParam ℤ) (o : outParam X)
-    extends TileStructureData D κ C S o where
+    (D κ : outParam ℝ) (S : outParam ℤ) (o : outParam X)
+    extends TileStructureData D κ S o where
   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
@@ -106,46 +109,50 @@ class TileStructure [FunctionDistances ℝ X] (Q : outParam (X → Θ X))
 
 export TileStructure (biUnion_Ω disjoint_Ω relative_fundamental_dyadic cdist_subset subset_cdist)
 
-def tile_existence {a : ℝ} [CompatibleFunctions ℝ X (2 ^ a)] [GridStructure X D κ C S o]
+def tile_existence {a : ℝ} [CompatibleFunctions ℝ X (2 ^ a)] [GridStructure X D κ S o]
     (ha : 4 ≤ a) {σ₁ σ₂ : X → ℤ} (hσ : σ₁ ≤ σ₂)
     (hσ₁ : Measurable σ₁) (hσ₂ : Measurable σ₂)
     {F G : Set X} (hF : Measurable F) (hG : Measurable G)
     (h2F : F ⊆ ball o (D ^ S)) (h2G : G ⊆ ball o (D ^ S))
     (hσ₁S : range σ₁ ⊆ Icc (-S) S) (hσ₂S : range σ₂ ⊆ Icc (-S) S)
     (Q : SimpleFunc X (Θ X)) :
-    TileStructure Q D κ C S o :=
+    TileStructure Q D κ S o :=
   sorry
 
-variable [FunctionDistances ℝ X] {Q : X → Θ X} [TileStructure Q D κ C S o]
+end DoublingMeasure
+
+open scoped ShortVariables
+variable {X : Type*} {a q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X}
+  [ProofData a q K σ₁ σ₂ F G] [TileStructure Q D κ S o]
 
 /- The set `E` defined in Proposition 2.0.2. -/
-def E (σ₁ σ₂ : X → ℤ) (p : 𝔓 X) : Set X :=
+def E (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 {p : 𝔓 X} {f : X → ℂ} {q : ℝ≥0∞}
 
-/- The operator `T` defined in Proposition 2.0.2, 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.0.2 is therefore `applied to `(F := Set.univ)`. -/
-def T (f : X → ℂ) : X → ℂ :=
-  indicator (E σ₁ σ₂ p)
+def T (p : 𝔓 X) (f : X → ℂ) : X → ℂ :=
+  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 :=
-  by sorry
+-- lemma Memℒp_T (hf : Memℒp f q) : Memℒp (T p 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
+-- /- 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
 
-/- 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
-    map_add' := sorry
-    map_smul' := sorry
-    cont := by sorry
+-- /- 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
+--     map_add' := sorry
+--     map_smul' := sorry
+--     cont := by sorry
 
 end T
 
@@ -172,16 +179,10 @@ def smul (l : ℝ) (p : 𝔓 X) : TileLike X :=
 def TileLike.toTile (t : TileLike X) : Set (X × Θ X) :=
   t.fst ×ˢ t.snd
 
--- old
--- lemma isAntichain_iff_disjoint (𝔄 : Set (𝔓 X)) :
---     IsAntichain (·≤·) (toTileLike (X := X) '' 𝔄) ↔
---     ∀ p p', p ∈ 𝔄 → p' ∈ 𝔄 → p ≠ p' →
---     Disjoint (toTileLike (X := X) p).toTile (toTileLike p').toTile := sorry
-
-def E₁ (G : Set X) (Q : X → Θ X) (t : TileLike X) : Set X :=
+def E₁ (t : TileLike X) : Set X :=
   t.1 ∩ G ∩ Q ⁻¹' t.2
 
-def E₂ (G : Set X) (Q : X → Θ X) (l : ℝ) (p : 𝔓 X) : Set X :=
+def E₂ (l : ℝ) (p : 𝔓 X) : Set X :=
   𝓓 (𝓘 p) ∩ G ∩ Q ⁻¹' ball_(D, p) (𝒬 p) l
 
 /-- `downClosure 𝔓'` is denoted `𝔓(𝔓') in the blueprint. It is the lower closure of `𝔓'` in `𝔓 X` w.r.t. to the relation `p ≤ p' := 𝓓 (𝓘 p) ⊆ 𝓓 (𝓘 p')`.
@@ -190,18 +191,35 @@ def downClosure (𝔓' : Set (𝔓 X)) : Set (𝔓 X) :=
   { p | ∃ p' ∈ 𝔓', 𝓓 (𝓘 p) ⊆ 𝓓 (𝓘 p') }
 
 /-- This density is defined to live in `ℝ≥0∞`. Use `ENNReal.toReal` to get a real number. -/
-def dens₁ (a : ℝ) (G : Set X) (Q : X → Θ X) (𝔓' : Set (𝔓 X)) : ℝ≥0∞ :=
+def dens₁ (𝔓' : Set (𝔓 X)) : ℝ≥0∞ :=
   ⨆ (p ∈ 𝔓') (l ≥ (2 : ℝ≥0)), l ^ (-a) *
   ⨆ (p' ∈ downClosure 𝔓') (_h2 : smul l p ≤ smul l p'),
-  volume (E₂ G Q l p) / volume (𝓓 (𝓘 p))
+  volume (E₂ l p) / volume (𝓓 (𝓘 p))
 
 /-- This density is defined to live in `ℝ≥0∞`. Use `ENNReal.toReal` to get a real number. -/
-def dens₂ (F : Set X) (𝔓' : Set (𝔓 X)) : ℝ≥0∞ :=
+def dens₂ (𝔓' : Set (𝔓 X)) : ℝ≥0∞ :=
   ⨆ (p ∈ 𝔓') (r ≥ 4 * D ^ 𝔰 p),
   volume (F ∩ ball (𝔠 p) r) / volume (ball (𝔠 p) r)
 
-/- Move to AntichainOperator file -/
--- prop 3
+-- a small characterization that might be useful
+lemma isAntichain_iff_disjoint (𝔄 : Set (𝔓 X)) :
+    IsAntichain (·≤·) (toTileLike (X := X) '' 𝔄) ↔
+    ∀ p p', p ∈ 𝔄 → p' ∈ 𝔄 → p ≠ p' →
+    Disjoint (toTileLike (X := X) p).toTile (toTileLike p').toTile := sorry
+
+/-- Constant appearing in Proposition 2.0.3. -/
+def C_2_0_3 (a q : ℝ) : ℝ := 2 ^ (150 * a ^ 3) / (q - 1)
+
+/-- Proposition 2.0.3 -/
+theorem antichain_operator {𝔄 : Set (𝔓 X)} {f g : X → ℂ} {q : ℝ}
+    (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x)
+    (hg : ∀ x, ‖g x‖ ≤ G.indicator 1 x)
+    (h𝔄 : IsAntichain (·≤·) (toTileLike (X := X) '' 𝔄))
+    : -- add conditions on q
+    ‖∫ x, conj (g x) * ∑ᶠ p : 𝔄, T p f x‖ ≤
+    C_2_0_3 a q * (dens₁ 𝔄).toReal ^ ((q - 1) / (8 * a ^ 4)) * (dens₂ 𝔄).toReal ^ (q⁻¹ - 2⁻¹) *
+    (snorm f 2 volume).toReal * (snorm g 2 volume).toReal := sorry
+
 
 
 --below is old
@@ -235,7 +253,7 @@ instance : Preorder (Tree X) := Preorder.lift Tree.carrier
 
 -- LaTeX note: $D ^ {s(p)}$ should be $D ^ {s(I(p))}$
 class Tree.IsThin (𝔗 : Tree X) : Prop where
-  thin {p : 𝔓 X} (hp : p ∈ 𝔗) : ball (𝔠 p) (8 * A ^ 3 * D ^ 𝔰 p) ⊆ 𝓓 (𝓘 𝔗.top)
+  thin {p : 𝔓 X} (hp : p ∈ 𝔗) : ball (𝔠 p) (8 * a/-fix-/ * D ^ 𝔰 p) ⊆ 𝓓 (𝓘 𝔗.top)
 
 alias Tree.thin := Tree.IsThin.thin
 
diff --git a/Carleson/MetricCarleson.lean b/Carleson/MetricCarleson.lean
index 52807ab7..30b630dd 100644
--- a/Carleson/MetricCarleson.lean
+++ b/Carleson/MetricCarleson.lean
@@ -6,7 +6,7 @@ open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators
 open scoped ENNReal
 noncomputable section
 
-/- The constant used in theorem1_2 -/
+/- The constant used in `metric_carleson` -/
 def C1_2 (a q : ℝ) : ℝ := 2 ^ (450 * a ^ 3) / (q - 1) ^ 5
 
 lemma C1_2_pos {a q : ℝ} (hq : 1 < q) : 0 < C1_2 a q := by
@@ -29,8 +29,7 @@ lemma C1_2_pos {a q : ℝ} (hq : 1 < q) : 0 < C1_2 a q := by
 
 section -- todo: old code
 
-variable {X : Type*} {a : ℝ} [MetricSpace X]
-  [DoublingMeasure X (2 ^ a)] [Inhabited X]
+variable {X : Type*} {a : ℝ} [MetricSpace X] [DoublingMeasure X (2 ^ a)] [Inhabited X]
 variable {τ q q' : ℝ} {C : ℝ}
 variable {F G : Set X}
 variable (K : X → X → ℂ)
@@ -133,11 +132,7 @@ 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 ∞ volume) (h2g : volume (support g) < ∞)
-      (h3g : Memℒp g 2 volume),
-      snorm (ANCZOperator K g) 2 volume ≤ 2 ^ a ^ 3 * snorm g 2 volume)
+    (hT : HasBoundedStrongType (ANCZOperator K) volume volume 2 2 (C_Ts a))
     (f : X → ℂ) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
     ∫⁻ x in G, CarlesonOperator K f x ≤
     ENNReal.ofReal (C1_2 a q) * (volume G) ^ q'⁻¹ * (volume F) ^ q⁻¹ := by
diff --git a/Carleson/Psi.lean b/Carleson/Psi.lean
index 1a789318..65b4648f 100644
--- a/Carleson/Psi.lean
+++ b/Carleson/Psi.lean
@@ -12,6 +12,9 @@ variable {D : ℝ} {s : ℤ} {K : X → X → ℂ}  {x y : X}
 def ψ (D x : ℝ) : ℝ :=
   max 0 <| min 1 <| min (4 * D * x - 1) (2 - 2 * x)
 
+set_option hygiene false
+scoped[ShortVariables] notation "ψ" => ψ (defaultD a)
+
 
 lemma support_ψ : support (ψ D) = Ioo (4 * D)⁻¹ 2⁻¹ := sorry
 lemma lipschitzWith_ψ (D : ℝ≥0) : LipschitzWith (4 * D) (ψ D) := sorry
diff --git a/Carleson/Theorem1_1/Carleson_on_the_real_line.lean b/Carleson/Theorem1_1/Carleson_on_the_real_line.lean
index 11bfe0cf..2c66fd0f 100644
--- a/Carleson/Theorem1_1/Carleson_on_the_real_line.lean
+++ b/Carleson/Theorem1_1/Carleson_on_the_real_line.lean
@@ -449,9 +449,7 @@ instance h6 : IsCZKernel 4 K where
   measurable := Hilbert_kernel_measurable
 
 /- Lemma ?-/
-lemma h3 (g : ℝ → ℂ) (hg : Memℒp g ∞ volume) (h2g : volume (support g) < ∞)
-    (h3g : Memℒp g 2 volume) :
-    snorm (ANCZOperator K g) 2 volume ≤ 2 ^ (4 : ℝ) ^ 3 * snorm g 2 volume := sorry
+lemma h3 : HasBoundedStrongType (ANCZOperator K) volume volume 2 2 (C_Ts 4) := sorry
 
 
 
diff --git a/blueprint/.gitignore b/blueprint/.gitignore
index a50e5c81..6f63206e 100644
--- a/blueprint/.gitignore
+++ b/blueprint/.gitignore
@@ -14,3 +14,6 @@ __pycache__
 *.mtc
 *.mtc0
 build
+*.bcf
+*.bbl
+*.toc
\ No newline at end of file
diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex
index b3170a1c..b3df5868 100644
--- a/blueprint/src/chapter/main.tex
+++ b/blueprint/src/chapter/main.tex
@@ -301,6 +301,8 @@ \chapter{Proof of Metric Space Carleson, overview}
 For any dyadic cube  $I$ and any $t$ with $tD^{s(I)} \ge D^{-S}$,
 \begin{equation}
         \label{eq-small-boundary}
+        % Note(Georges Gonthier): The D in the RHS can be replaced by 2.
+        % We can do the same in the statement and proof of {boundary-measure}.
         \mu(\{x \in I \ : \ \rho(x, X \setminus I) \leq t D^{s(I)}\}) \le D t^\kappa \mu(I)\,.
     \end{equation}
 
@@ -1823,10 +1825,12 @@ \section{Organisation of the tiles}\label{subsectilesorg}
 \begin{equation}\label{definegone}
     G_1:=\bigcup_{\fp\in \fP_{F,G} }\scI(\fp)\, .
 \end{equation}
-For an integer $\lambda\ge 0$, define  $A(\lambda,k,n)$ to be the set  of all $x\in X$ such that
+For an integer $\lambda\ge 0$, define  $A(\lambda,k,n)$ to be the set
+of all $x\in X$ such that
 \begin{equation}
     \label{eq-Aoverlap-def}
-    \sum_{\fp \in \mathfrak{M}(k,n)}\mathbf{1}_{\scI(\fp)}(x)>1+\lambda 2^{n+1}
+    % remark(F): replaced > by \ge
+    \sum_{\fp \in \mathfrak{M}(k,n)}\mathbf{1}_{\scI(\fp)}(x)\ge 1+\lambda 2^{n+1}
 \end{equation}
 and define
 \begin{equation}\label{definegone2}
@@ -2119,23 +2123,25 @@ \section{Proof of the Exceptional Sets Lemma}
  \uses{John-Nirenberg}
     We have
     \begin{equation}\label{eq-musum}
-        \sum_{\mathfrak{m} \in \mathfrak{M}(k,n)} \mu(\scI(\mathfrak{m}))\le 2^{n+1}2^{k+1}\mu(G).
+        % Note(Georges Gonthier): new factor suggested by
+        \sum_{\mathfrak{m} \in \mathfrak{M}(k,n)} \mu(\scI(\mathfrak{m}))\le 2^{n+k+3}\mu(G).
     \end{equation}
 \end{lemma}
 \begin{proof}
-    We write the left-hand side of \eqref{eq-musum}
+% Note(Georges Gonthier): sum should start at 0, not 1
+        We write the left-hand side of \eqref{eq-musum}
 \begin{equation}
-    \int \sum_{\mathfrak{m} \in \mathfrak{M}(k,n)} \mathbf{1}_{\scI(\mathfrak{m})}(x) \, d\mu(x) \le
-2^{n+1} \sum_{\lambda=1}^{|\mathfrak{M}|}\mu(A(\lambda, k,n))\,.
+    \int \sum_{\mathfrak{m} \in \mathfrak{M}(k,n)} \mathbf{0}_{\scI(\mathfrak{m})}(x) \, d\mu(x) \le
+2^{n+1} \sum_{\lambda=0}^{|\mathfrak{M}|}\mu(A(\lambda, k,n))\,.
 \end{equation}
 Using \Cref{John-Nirenberg}
 and then summing a geometric series, we estimate this by
 \begin{equation}
     \le
-2^{n+1}\sum_{\lambda=1}^{|\mathfrak{M}|}
+2^{n+1}\sum_{\lambda=0}^{|\mathfrak{M}|}
 2^{k+1-\lambda}\mu(G)
 \le
-2^{n+1}2^{k+1}\mu(G)\, .
+2^{n+1}2^{k+2}\mu(G)\, .
 \end{equation}
 This proves the lemma.
 \end{proof}
@@ -2262,7 +2268,7 @@ \section{Proof of the Exceptional Sets Lemma}
 
     \begin{lemma}[third exception]
     \label{third-exception}
-\uses{tree-count,boundary-exception}
+\uses{tree-count,boundary-exception, top-tiles}
        We have
 \begin{equation}
     \mu(G_3)\le 2^{-4} \mu(G)\, .
@@ -2376,17 +2382,18 @@ \section{Auxiliary lemmas}
 \label{wiggle-order-3}
 \uses{wiggle-order-1, wiggle-order-2}
     The following implications hold for all $\fq, \fq' \in \fP$:
+    % Note: some fixes were suggested by Georges Gonthier
     \begin{equation}
         \label{eq-sc1}
-        \fq \lesssim \fq' \ \text{and} \ \lambda \ge 1 \implies \lambda \fq \lesssim \lambda \fq'\,,
+        \fq \le \fq' \ \text{and} \ \lambda \ge 2 \implies \lambda \fq \lesssim \lambda \fq'\,,
     \end{equation}
     \begin{equation}
         \label{eq-sc2}
-        10\fq \lesssim \fq' \ \text{and} \ \fq \ne \fq' \implies 100 \fq \lesssim 100 \fq'\,,
+        10\fq \lesssim \fq' \ \text{and} \ \scI(\fq) \ne \scI(\fq') \implies 100 \fq \lesssim 100 \fq'\,,
     \end{equation}
     \begin{equation}
         \label{eq-sc3}
-        2\fq \lesssim \fq' \ \text{and} \ \fq \ne \fq' \implies 4 \fq \lesssim 500 \fq'\,.
+        2\fq \lesssim \fq' \ \text{and} \ \scI(\fq) \ne \scI(\fq') \implies 4 \fq \lesssim 500 \fq'\,.
     \end{equation}
 \end{lemma}