Update ClassicalCarleson.lean

fpvandoorn · Jul 25, 2024 · 9baa785 · 9baa785
1 parent d948d00
commit 9baa785
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Carleson/Classical/ClassicalCarleson.lean b/Carleson/Classical/ClassicalCarleson.lean
@@ -25,7 +25,7 @@ theorem classical_carleson {f : ℝ → ℂ}
   obtain ⟨N₀, hN₀⟩ := fourierConv_ofTwiceDifferentiable periodic_f₀ ((contDiff_top.mp (contDiff_f₀)) 2) ε4pos
 
   set h := f₀ - f with hdef
-  have h_measurable : Measurable h := Continuous.measurable (Continuous.sub contDiff_f₀.continuous unicontf.continuous)
+  have h_measurable : Measurable h := (Continuous.sub contDiff_f₀.continuous unicontf.continuous).measurable
   have h_periodic : h.Periodic (2 * Real.pi) := periodic_f₀.sub periodicf
   have h_bound : ∀ x, Complex.abs (h x) ≤ ε' := by
     intro x