put hypotheses shared in chapters 2-7 in a class

also do some blueprint fixes

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𝔰)

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

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