enormify most of the lemmas (#464)

Remove uses of `‖...‖₊` in favour of `‖...‖ₑ` except for
`TileCorrelation.lean`.

----

I won't have time to continue on this immediately because I'll be on
vacation climbing Mount Fuji from 19 to 26 July. But this can be merged
as-is.

Author: Parcly-Taxel

Carleson/Antichain/Basic.lean

@@ -87,84 +87,56 @@ lemma C6_1_2_ne_zero (a : ℕ) : (C6_1_2 a : ℝ≥0∞) ≠ 0 := by rw [C6_1_2]
 open MeasureTheory Metric Bornology Set
 
 private lemma ineq_6_1_7 (x : X) {𝔄 : Set (𝔓 X)} (p : 𝔄) :
-    (2 : ℝ≥0) ^ a ^ 3 / volume.real (ball x (↑D ^ 𝔰 p.1 / (↑D * 4))) ≤
-      2 ^ (5 * a + 101 * a ^ 3) / volume.real (ball x (8 * ↑D ^ 𝔰 p.1)) := by
-  calc (2 : ℝ≥0) ^ a ^ 3 / volume.real (ball x ((D : ℝ) ^ 𝔰 p.1 / (↑D * 4)))
-    _ = 2 ^ a ^ 3 / volume.real (ball x ((1 / ((D : ℝ) * 32)) * (8 * D ^ 𝔰 p.1))) := by
-      congr
-      ring_nf
+    (2 : ℝ≥0∞) ^ a ^ 3 / volume (ball x (D ^ 𝔰 p.1 / (D * 4))) ≤
+    2 ^ (5 * a + 101 * a ^ 3) / volume (ball x (8 * D ^ 𝔰 p.1)) := by
+  calc
+    _ = 2 ^ a ^ 3 / volume (ball x (1 / (D * 32) * (8 * D ^ 𝔰 p.1))) := by congr! 3; ring
     _ = 2 ^ a ^ 3 * 2 ^ (5 * a + 100 * a ^ 3) / (2 ^ (5 * a + 100 * a ^ 3) *
-          volume.real (ball x ((1 / ((D : ℝ) * 32)) * (8 * D ^ 𝔰 p.1)))) := by
-        have hvol : volume.real (ball x (1 / ↑D / 32 * (8 * ↑D ^ 𝔰 p.1))) ≠ 0 :=
-          ne_of_gt (measureReal_ball_pos _
-            (mul_pos (div_pos (one_div_pos.mpr (defaultD_pos _)) (by positivity))
-              (mul_pos (by positivity) (zpow_pos (defaultD_pos _) _))))
-        rw [mul_div_assoc, ← div_div, div_eq_mul_inv]
-        congr
-        rw [eq_div_iff_mul_eq (by positivity), mul_comm, mul_assoc,
-          mul_inv_cancel₀ hvol, mul_one]
-    _ ≤ 2 ^ a ^ 3 * 2 ^ (5 * a + 100 * a ^ 3) / volume.real (ball x (8 * D ^ 𝔰 p.1)) := by
+        volume (ball x (1 / (D * 32) * (8 * D ^ 𝔰 p.1)))) := by
+      rw [mul_div_assoc, ← div_div, div_eq_mul_inv]
+      conv_rhs => rw [← inv_inv (volume _), ← div_eq_mul_inv,
+        ENNReal.div_div_cancel (by positivity) (by finiteness)]
+    _ ≤ 2 ^ a ^ 3 * 2 ^ (5 * a + 100 * a ^ 3) / volume (ball x (8 * D ^ 𝔰 p.1)) := by
       gcongr
-      · exact (measureReal_ball_pos x (mul_pos (by positivity) (zpow_pos (defaultD_pos _) _)))
-      · have heq : 2 ^ (100 * a ^ 2) * 2 ^ 5 * (1 / (↑D * 32) * (8 * (D : ℝ) ^ 𝔰 p.1)) =
-            (8 * ↑D ^ 𝔰 p.1) := by
+      · have heq : 2 ^ (100 * a ^ 2) * 2 ^ 5 * (1 / (D * 32) * (8 * (D : ℝ) ^ 𝔰 p.1)) =
+            8 * D ^ 𝔰 p.1 := by
           have hD : (D : ℝ) = 2 ^ (100 * a^2) := by simp
           rw [← hD]
           ring_nf
           rw [mul_inv_cancel₀ (defaultD_pos _).ne', one_mul]
-        convert (DoublingMeasure.volume_real_ball_two_le_same_repeat x
-          ((1 / ((D : ℝ) * 32)) * (8 * D ^ 𝔰 p.1)) (100*a^2 + 5)) using 1
+        convert measure_ball_two_le_same_iterate (μ := volume) x
+          (1 / (D * 32) * (8 * D ^ 𝔰 p.1)) (100*a^2 + 5) using 2
         · conv_lhs => rw [← heq, ← pow_add]
-        · congr 1
-          simp only [defaultA, Nat.cast_pow, Nat.cast_ofNat]
-          ring
-    _ = 2 ^ (5 * a + 101 * a ^ 3) / volume.real (ball x (8 * ↑D ^ 𝔰 p.1)) := by ring_nf
-
-private lemma ineq_6_1_7' (x : X) {𝔄 : Set (𝔓 X)} (p : 𝔄) :
-    (2 : ℝ≥0) ^ a ^ 3 / (volume (ball x (↑D ^ 𝔰 p.1 / (↑D * 4)))).toNNReal ≤
-      2 ^ (5 * a + 101 * a ^ 3) / (volume (ball x (8 * ↑D ^ 𝔰 p.1))).toNNReal := by
-  suffices (2 : ℝ≥0) ^ a ^ 3 / volume.real (ball x (↑D ^ 𝔰 p.1 / (↑D * 4))) ≤
-      2 ^ (5 * a + 101 * a ^ 3) / volume.real (ball x (8 * ↑D ^ 𝔰 p.1)) by
-    simp only [← NNReal.coe_le_coe, ← NNReal.val_eq_coe]
-    exact this
-  exact ineq_6_1_7 x p
+        · rw [Nat.cast_pow, Nat.cast_ofNat, ENNReal.coe_pow, coe_ofNat]; ring
+    _ = _ := by ring_nf
 
 -- Composition of inequalities 6.1.6, 6.1.7, 6.1.8.
 lemma norm_Ks_le' {x y : X} {𝔄 : Set (𝔓 X)} (p : 𝔄) (hxE : x ∈ E ↑p) (hy : Ks (𝔰 p.1) x y ≠ 0) :
-    ‖Ks (𝔰 p.1) x y‖₊ ≤
-      (2 : ℝ≥0) ^ (6*a + 101*a^3) / (volume (ball (𝔠 p.1) (8*D ^ 𝔰 p.1))).toNNReal := by
+    ‖Ks (𝔰 p.1) x y‖ₑ ≤ 2 ^ (6 * a + 101 * a ^ 3) / volume (ball (𝔠 p.1) (8 * D ^ 𝔰 p.1)) := by
   have hDpow_pos : 0 < (D : ℝ) ^ 𝔰 p.1 := defaultD_pow_pos ..
   have h8Dpow_pos : 0 < 8 * (D : ℝ) ^ 𝔰 p.1 := mul_defaultD_pow_pos _ (by linarith) _
-  have hdist_cp : dist x (𝔠 p) ≤ 4*D ^ 𝔰 p.1 := le_of_lt (mem_ball.mp (Grid_subset_ball hxE.1))
-  have h : ‖Ks (𝔰 p.1) x y‖₊ ≤ (2 : ℝ≥0)^(a^3) / (volume (ball x (D ^ (𝔰 p.1 - 1)/4))).toNNReal := by
-    apply le_trans (NNReal.coe_le_coe.mpr kernel_bound_old)
-    rw [NNReal.coe_div, NNReal.coe_pow, NNReal.coe_ofNat, ← NNReal.val_eq_coe]
-    exact div_le_div_of_nonneg_left (pow_nonneg zero_le_two _)
-      (measure_ball_pos_real x _ (div_pos (zpow_pos (defaultD_pos _) _) zero_lt_four))
-      (measureReal_mono (Metric.ball_subset_ball (dist_mem_Icc_of_Ks_ne_zero hy).1)
-        measure_ball_ne_top)
-  apply le_trans h
+  have hdist_cp : dist x (𝔠 p) ≤ 4 * D ^ 𝔰 p.1 := (mem_ball.mp (Grid_subset_ball hxE.1)).le
+  have h : ‖Ks (𝔰 p.1) x y‖ₑ ≤ 2 ^ a ^ 3 / volume (ball x (D ^ (𝔰 p.1 - 1) / 4)) := by
+    apply kernel_bound.trans
+    rw [C_K, ← Nat.cast_pow, NNReal.rpow_natCast, ENNReal.coe_pow, coe_ofNat, vol]; gcongr
+    exact (dist_mem_Icc_of_Ks_ne_zero hy).1
+  apply h.trans
   rw [zpow_sub₀ (by simp), zpow_one, div_div]
-  apply le_trans (ineq_6_1_7' x p)
+  apply (ineq_6_1_7 x p).trans
   have ha : 6 * a + 101 * a ^ 3 = (5 * a + 101 * a ^ 3) + a := by omega
   simp only [div_eq_mul_inv, ge_iff_le]
   rw [ha, pow_add _ (5 * a + 101 * a ^ 3) a, mul_assoc]
   apply mul_le_mul_of_nonneg_left _ (zero_le _)
-  suffices (volume (ball (𝔠 p.1) (8 * ↑D ^ 𝔰 p.1))).toNNReal ≤
-      2 ^ a * (volume (ball x (8 * ↑D ^ 𝔰 p.1))).toNNReal by
-    rw [le_mul_inv_iff₀, ← le_inv_mul_iff₀ , mul_comm _ (_^a), inv_inv]
-    exact this
-    · exact inv_pos.mpr (measure_ball_pos_nnreal _ _ h8Dpow_pos)
-    · exact measure_ball_pos_nnreal _ _ h8Dpow_pos
-  have h2 : dist x (𝔠 p) + 8 * ↑D ^ 𝔰 p.1 ≤ 2 * (8 * ↑D ^ 𝔰 p.1) :=
-    calc dist x (𝔠 p) + 8 * ↑D ^ 𝔰 p.1
-      ≤ 4 * ↑D ^ 𝔰 p.1 + 8 * ↑D ^ 𝔰 p.1 := (add_le_add_iff_right _).mpr hdist_cp
-    _ ≤ 2 * (8 * ↑D ^ 𝔰 p.1) := by
-      ring_nf
-      exact mul_le_mul_of_nonneg (le_refl _) (by linarith) (le_of_lt hDpow_pos) (by linarith)
-  convert measureNNReal_ball_le_of_dist_le' (μ := volume) zero_lt_two h2
-  simp only [As, defaultA, Nat.cast_pow, Nat.cast_ofNat, Nat.one_lt_ofNat, logb_self_eq_one,
-    Nat.ceil_one, pow_one]
+  suffices volume (ball (𝔠 p.1) (8 * D ^ 𝔰 p.1)) ≤ 2 ^ a * volume (ball x (8 * D ^ 𝔰 p.1)) by
+    rw [← inv_inv (2 ^ a), ← ENNReal.mul_inv (.inl (by simp)) (.inl (by finiteness)),
+      ENNReal.inv_le_inv, ← ENNReal.div_eq_inv_mul]
+    exact ENNReal.div_le_of_le_mul' this
+  have h2 : dist x (𝔠 p) + 8 * D ^ 𝔰 p.1 ≤ 2 * (8 * D ^ 𝔰 p.1) :=
+    calc
+      _ ≤ (4 : ℝ) * D ^ 𝔰 p.1 + 8 * D ^ 𝔰 p.1 := (add_le_add_iff_right _).mpr hdist_cp
+      _ ≤ _ := by linarith
+  convert measure_ball_le_of_dist_le' (μ := volume) zero_lt_two h2
+  simp [As]
 
 -- lemma 6.1.2
 lemma MaximalBoundAntichain {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ ·) 𝔄)
@@ -198,75 +170,62 @@ lemma MaximalBoundAntichain {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ 
         rw [div_eq_inv_mul, ← add_mul]
         exact mul_lt_mul_of_pos_right (by norm_num) (defaultD_pow_pos ..)
     -- 6.1.6, 6.1.7, 6.1.8
-    have hKs : ∀ (y : X) (hy : Ks (𝔰 p.1) x y ≠ 0), ‖Ks (𝔰 p.1) x y‖₊ ≤
-        (2 : ℝ≥0) ^ (6*a + 101*a^3) / (volume (ball (𝔠 p.1) (8*D ^ 𝔰 p.1))).toNNReal :=
-      fun y hy ↦ norm_Ks_le' _ hxE hy
-    calc (‖carlesonSum 𝔄 f x‖₊ : ℝ≥0∞)
-      = ↑‖carlesonOn p f x‖₊:= by
-          have hp : ↑p ∈ ({p | p ∈ 𝔄} : Finset (𝔓 X)) := by
-            simp only [Finset.mem_filter, Finset.mem_univ, Subtype.coe_prop, and_self]
-          rw [carlesonSum, Finset.sum_eq_single_of_mem p.1 hp hne_p]
-    _ ≤ ∫⁻ (y : X), ‖cexp (I * (↑((Q x) y) - ↑((Q x) x))) * Ks (𝔰 p.1) x y * f y‖ₑ := by
+    have hKs (y : X) (hy : Ks (𝔰 p.1) x y ≠ 0) :
+        ‖Ks (𝔰 p.1) x y‖ₑ ≤ 2 ^ (6 * a + 101 * a ^ 3) / volume (ball (𝔠 p.1) (8 * D ^ 𝔰 p.1)) :=
+      norm_Ks_le' _ hxE hy
+    calc
+    _ = ‖carlesonOn p f x‖ₑ := by
+        have hp : ↑p ∈ ({p | p ∈ 𝔄} : Finset (𝔓 X)) := by
+          simp only [Finset.mem_filter, Finset.mem_univ, Subtype.coe_prop, and_self]
+        rw [carlesonSum, Finset.sum_eq_single_of_mem p.1 hp hne_p]
+    _ ≤ ∫⁻ y, ‖exp (I * (Q x y - Q x x)) * Ks (𝔰 p.1) x y * f y‖ₑ := by
         rw [carlesonOn, indicator, if_pos hxE]
         refine le_trans (enorm_integral_le_lintegral_enorm _) (lintegral_mono fun z w h ↦ ?_)
         simp only [nnnorm_mul, coe_mul, some_eq_coe', zpow_neg, Ks, mul_assoc,
           enorm_eq_nnnorm] at h ⊢
         use w
-    _ ≤ ∫⁻ (y : X), ‖Ks (𝔰 p.1) x y * f y‖ₑ := by
-      simp only [enorm_mul]
-      refine lintegral_mono_nnreal fun y ↦ ?_
-      rw [mul_assoc]
-      conv_rhs => rw [← one_mul (‖Ks (𝔰 p.1) x y‖₊ * ‖f y‖₊)]
-      apply mul_le_mul_of_nonneg_right _ (zero_le _)
-      · apply le_of_eq
-        rw [mul_comm, ← Complex.ofReal_sub, NNReal.eq_iff,
-          coe_nnnorm, NNReal.coe_one, Complex.norm_exp_ofReal_mul_I]
-    _ = ∫⁻ (y : X) in ball (𝔠 ↑p) (8 * ↑D ^ 𝔰 p.1), ‖Ks (𝔰 p.1) x y * f y‖ₑ := by
-        rw [MeasureTheory.setLIntegral_eq_of_support_subset]
+    _ ≤ ∫⁻ y, ‖Ks (𝔰 p.1) x y * f y‖ₑ := by
+      simp only [enorm_mul]; refine lintegral_mono_fn fun y ↦ ?_
+      rw [← Complex.ofReal_sub, enorm_exp_I_mul_ofReal, one_mul]
+    _ = ∫⁻ y in ball (𝔠 p) (8 * D ^ 𝔰 p.1), ‖Ks (𝔰 p.1) x y * f y‖ₑ := by
+        rw [setLIntegral_eq_of_support_subset]
         intro y hy
         simp only [enorm_mul, Function.support_mul, mem_inter_iff, Function.mem_support, ne_eq,
           enorm_eq_zero] at hy
         rw [mem_ball, dist_comm]
         exact hdist_cpy y hy.1
-    _ ≤ ∫⁻ (y : X) in ball (𝔠 ↑p) (8 * ↑D ^ 𝔰 p.1),
-        (((2 : ℝ≥0) ^ (6*a + 101*a^3) /
-          (volume (ball (𝔠 p.1) (8*D ^ 𝔰 p.1))).toNNReal) * ‖f y‖₊ : ℝ≥0) := by
-      refine lintegral_mono_nnreal fun y ↦ ?_
-      rw [nnnorm_mul]
-      gcongr
+    _ ≤ ∫⁻ y in ball (𝔠 p) (8 * D ^ 𝔰 p.1),
+        2 ^ (6 * a + 101 * a ^ 3) / volume (ball (𝔠 p.1) (8 * D ^ 𝔰 p.1)) * ‖f y‖ₑ := by
+      refine lintegral_mono_fn fun y ↦ ?_
+      rw [enorm_mul]; gcongr
       by_cases hy : Ks (𝔰 p.1) x y = 0
       · simp [hy]
       · exact hKs y hy
-    _ = (2 : ℝ≥0)^(5*a + 101*a^3 + a) *
-        ⨍⁻ y, ‖f y‖ₑ ∂volume.restrict (ball (𝔠 p.1) (8*D ^ 𝔰 p.1)) := by
-      rw [laverage_eq, Measure.restrict_apply MeasurableSet.univ, univ_inter]
-      simp_rw [div_eq_mul_inv, coe_mul, enorm_eq_nnnorm]
-      rw [lintegral_const_mul _ hfm.nnnorm.coe_nnreal_ennreal, ENNReal.coe_pow, coe_inv
-        (ne_of_gt (measure_ball_pos_nnreal _ _ h8Dpow_pos)),
-        ENNReal.coe_toNNReal measure_ball_ne_top]
-      ring
-    _ ≤ (C6_1_2 a) * (ball (𝔠 p.1) (8*D ^ 𝔰 p.1)).indicator (x := x)
-        (fun _ ↦ ⨍⁻ y, ‖f y‖ₑ ∂volume.restrict (ball (𝔠 p.1) (8*D ^ 𝔰 p.1))) := by
-      simp only [coe_ofNat, indicator, mem_ball, mul_ite, mul_zero]
+    _ = 2 ^ (5 * a + 101 * a ^ 3 + a) * ⨍⁻ y in ball (𝔠 p.1) (8 * D ^ 𝔰 p.1), ‖f y‖ₑ ∂volume := by
+      rw [lintegral_const_mul _ hfm.enorm, ENNReal.mul_comm_div, setLAverage_eq]
+      congr 2; ring
+    _ ≤ C6_1_2 a * (ball (𝔠 p.1) (8 * D ^ 𝔰 p.1)).indicator (x := x)
+        (fun _ ↦ ⨍⁻ y in ball (𝔠 p.1) (8 * D ^ 𝔰 p.1), ‖f y‖ₑ ∂volume) := by
+      simp only [indicator, mem_ball, mul_ite, mul_zero]
       rw [if_pos]
       · gcongr
-        rw [C6_1_2, add_comm (5*a), add_assoc]; norm_cast
+        rw [C6_1_2, add_comm (5 * a), add_assoc]; norm_cast
         apply pow_le_pow_right₀ one_le_two
         calc
-        _ ≤ 101 * a ^ 3  + 6 * a ^ 3:= by
+        _ ≤ 101 * a ^ 3 + 6 * a ^ 3 := by
           rw [add_le_add_iff_left]
           ring_nf
           gcongr
           exact le_self_pow₀ (by linarith [four_le_a X]) (by omega)
         _ = 107 * a ^ 3 := by ring
-      · exact lt_of_le_of_lt hdist_cp
+      · exact hdist_cp.trans_lt
           (mul_lt_mul_of_nonneg_of_pos (by linarith) (le_refl _) (by linarith) hDpow_pos)
-    _ ≤ (C6_1_2 a) * MB volume 𝔄 𝔠 (fun 𝔭 ↦ 8*D ^ 𝔰 𝔭) f x := by
+    _ ≤ C6_1_2 a * MB volume 𝔄 𝔠 (8 * D ^ 𝔰 ·) f x := by
       rw [mul_le_mul_left (C6_1_2_ne_zero a) coe_ne_top, MB, maximalFunction,
         inv_one, ENNReal.rpow_one, le_iSup_iff]
       simp only [iSup_le_iff, ENNReal.rpow_one]
       exact (fun _ hc ↦ hc p.1 p.2)
-  · simp only [ne_eq, Subtype.exists, exists_prop, not_exists, not_and, Decidable.not_not] at hx
+  · simp only [ne_eq, Subtype.exists, exists_prop, not_exists, not_and, not_not] at hx
     have h0 : carlesonSum 𝔄 f x = 0 := by
       refine Finset.sum_eq_zero (fun p hp ↦ ?_)
       rw [Finset.mem_filter_univ] at hp

Carleson/Antichain/TileCorrelation.lean

@@ -79,10 +79,9 @@ lemma aux_6_2_3 (s₁ s₂ : ℤ) (x₁ x₂ y y' : X) :
   C2_1_3 a / volume (ball x₂ (D ^ s₂)) *
   (D2_1_3 a / volume (ball x₁ (D ^ s₁)) * (edist y y' ^ τ / (D ^ s₁) ^ τ)) := by
   apply mul_le_mul enorm_Ks_le _ (zero_le _) (zero_le _)
-  convert nnnorm_Ks_sub_Ks_le
+  convert enorm_Ks_sub_Ks_le
   rw [← ENNReal.div_rpow_of_nonneg _ _ (τ_nonneg X)]
-  simp only [defaultτ]; congr
-  simp only [coe_nnreal_ennreal_nndist]
+  simp only [defaultτ]
 
 /-- Equation (6.2.5) of Lemma 6.2.1. -/
 lemma e625 {s₁ s₂ : ℤ} {x₁ x₂ y y' : X} (hy' : y ≠ y') (hs : s₁ ≤ s₂) :

Carleson/Classical/CarlesonOperatorReal.lean

@@ -11,7 +11,7 @@ open MeasureTheory
 --TODO: avoid this extra definition?
 def carlesonOperatorReal (K : ℝ → ℝ → ℂ) (f : ℝ → ℂ) (x : ℝ) : ENNReal :=
   ⨆ (n : ℤ) (r : ℝ) (_ : 0 < r) (_ : r < 1),
-  ↑‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * Complex.exp (Complex.I * n * y)‖₊
+  ‖∫ y in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * Complex.exp (Complex.I * n * y)‖ₑ
 
 
 lemma annulus_real_eq {x r R : ℝ} (r_nonneg : 0 ≤ r) : {y | dist x y ∈ Set.Ioo r R} = Set.Ioo (x - R) (x - r) ∪ Set.Ioo (x + r) (x + R) := by
@@ -79,9 +79,9 @@ lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
     fun x r y ↦
       {y | dist x y ∈ Set.Ioo r 1}.indicator (fun t ↦ f t * K x t * (Complex.I * ↑n * ↑t).exp) y
     with Fdef
-  set G : ℝ → ℝ → ENNReal := fun x r ↦ ↑‖∫ (y : ℝ), F x r y‖₊ with Gdef
-  have hFG : (fun x ↦ ⨆ r, ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ↑‖∫ (y : ℝ) in
-                {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊)
+  set G : ℝ → ℝ → ENNReal := fun x r ↦ ‖∫ (y : ℝ), F x r y‖ₑ with Gdef
+  have hFG : (fun x ↦ ⨆ r, ⨆ (_ : 0 < r), ⨆ (_ : r < 1), ‖∫ (y : ℝ) in
+                {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖ₑ)
              = fun x ↦ ⨆ (r : ℝ) (_ : r ∈ Set.Ioo 0 1), G x r := by
     ext
     congr with r
@@ -245,8 +245,8 @@ variable {α β : Type*} [MeasurableSpace α]
   -- then use measurable_iSup
 -/
 
-
-lemma carlesonOperatorReal_mul {f : ℝ → ℂ} {x : ℝ} {a : ℝ} (ha : 0 < a) : T f x = a.toNNReal * T (fun x ↦ 1 / a * f x) x := by
+lemma carlesonOperatorReal_mul {f : ℝ → ℂ} {x : ℝ} {a : ℝ} (ha : 0 < a) :
+    T f x = ENNReal.ofReal a * T (fun x ↦ 1 / a * f x) x := by
   rw [carlesonOperatorReal, carlesonOperatorReal, ENNReal.mul_iSup]
   congr with n
   rw [ENNReal.mul_iSup]
@@ -257,16 +257,10 @@ lemma carlesonOperatorReal_mul {f : ℝ → ℂ} {x : ℝ} {a : ℝ} (ha : 0 < a
   rw [ENNReal.mul_iSup]
   congr with rle1
   norm_cast
-  apply NNReal.eq
-  simp only [coe_nnnorm, NNReal.coe_mul]
-  rw [← Real.norm_of_nonneg NNReal.zero_le_coe, ← Complex.norm_real, ← norm_mul,
-    ← integral_const_mul, Real.coe_toNNReal a ha.le]
-  congr with y
-  field_simp
-  rw [mul_div_cancel_left₀]
-  norm_cast
-  exact ha.ne.symm
-
+  rw [← Real.enorm_eq_ofReal ha.le]
+  simp_rw [mul_assoc, integral_const_mul, enorm_mul, ← mul_assoc]
+  rw [← enorm_norm (Complex.ofReal (1 / a)), Complex.norm_real, enorm_norm, ← enorm_mul,
+    mul_one_div_cancel ha.ne', enorm_one, one_mul]
 
 lemma carlesonOperatorReal_eq_of_restrict_interval {f : ℝ → ℂ} {a b : ℝ} {x : ℝ} (hx : x ∈ Set.Icc a b) : T f x = T ((Set.Ioo (a - 1) (b + 1)).indicator f) x := by
   simp_rw [carlesonOperatorReal]