add measurability assumption in antichain_operator

fpvandoorn · Aug 14, 2024 · 8c8aaf3 · 8c8aaf3
1 parent 82413bf
commit 8c8aaf3
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Carleson/AntichainOperator.lean b/Carleson/AntichainOperator.lean
@@ -347,8 +347,8 @@ 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 → ℂ}
-    (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x)
-    (hg : ∀ x, ‖g x‖ ≤ G.indicator 1 x)
+    (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x)
+    (hg : Measurable g) (hg : ∀ x, ‖g x‖ ≤ G.indicator 1 x)
     (h𝔄 : IsAntichain (·≤·) (toTileLike (X := X) '' 𝔄)) :
     ‖∫ 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⁻¹) *