Update Hilbert_kernel.lean

fpvandoorn · Jun 15, 2024 · f22fdb7 · f22fdb7
1 parent 94e848d
commit f22fdb7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Carleson/Theorem1_1/Hilbert_kernel.lean b/Carleson/Theorem1_1/Hilbert_kernel.lean
@@ -23,7 +23,7 @@ lemma k_measurable : Measurable k := by
   apply Measurable.div
   . apply Measurable.comp'
     · exact Complex.measurable_ofReal
-    · exact Measurable.max (measurable_const.sub measurable_norm) measurable_const
+    · exact (measurable_const.sub measurable_norm).max measurable_const
   . measurability
 
 def K (x y : ℝ) : ℂ := k (x - y)