From abc6ac216aac9b97c13d13e5314970b3f7c4390c Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Thu, 20 Jun 2024 19:14:42 +0200
Subject: [PATCH] fix

---
 Carleson/FinitaryCarleson.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Carleson/FinitaryCarleson.lean b/Carleson/FinitaryCarleson.lean
index b3fc6e34..4330bd51 100644
--- a/Carleson/FinitaryCarleson.lean
+++ b/Carleson/FinitaryCarleson.lean
@@ -17,4 +17,4 @@ theorem finitary_carleson [ProofData a q K σ₁ σ₂ F G] :
     ∃ G', Measurable G' ∧ 2 * volume G' ≤ volume G ∧
     ∀ f : X → ℂ, Measurable f → (∀ x, ‖f x‖ ≤ F.indicator 1 x) →
     ∫⁻ x in G \ G', ‖∑ s in Icc (σ₁ x) (σ₂ x), ∫ y, Ks s x y * f y * exp (I * Q x y)‖₊ ≤
-    C2_0_1 a (nnq X) * (volume G) ^ (1 - 1 / q) * (volume F) ^ (1 / q) := by sorry
+    C2_0_1 a nnq * (volume G) ^ (1 - 1 / q) * (volume F) ^ (1 / q) := by sorry