oops, semantic merge conflict

fpvandoorn · Jul 12, 2024 · 5a83b4a · 5a83b4a
1 parent 46616d8
commit 5a83b4a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Carleson/FinitaryCarleson.lean b/Carleson/FinitaryCarleson.lean
@@ -7,7 +7,7 @@ noncomputable section
 
 open scoped ShortVariables
 variable {X : Type*} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X}
-  [MetricSpace X] [ProofData a q K σ₁ σ₂ F G]
+  [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q D κ S o]
 
 theorem integrable_tile_sum_operator
     {f : X → ℂ} (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) {x : X} {s : ℤ} :