From f22fdb7b034b3c0e904cee4175be08877eb76646 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sat, 15 Jun 2024 23:50:55 +0200
Subject: [PATCH] Update Hilbert_kernel.lean

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

diff --git a/Carleson/Theorem1_1/Hilbert_kernel.lean b/Carleson/Theorem1_1/Hilbert_kernel.lean
index 10870f2c..6ee13e2a 100644
--- 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)