From 386a3c6e178f3c1b92ad5547a69b48ebfe1564ea Mon Sep 17 00:00:00 2001
From: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Date: Mon, 6 Jan 2025 15:12:53 +0100
Subject: [PATCH] chore: bump Lean and Mathlib to v4.15 (#202)

This will conflict with #199: you can merge any of them first, but then
ask me to fix the conflicts.

---------

Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
---
 Carleson/Antichain/AntichainOperator.lean     |   7 +-
 Carleson/Classical/Approximation.lean         |  20 ++--
 Carleson/Classical/ClassicalCarleson.lean     |   2 +-
 .../Classical/ControlApproximationEffect.lean |  64 +++++++----
 Carleson/Classical/DirichletKernel.lean       |  10 +-
 Carleson/Discrete/ForestComplement.lean       |   2 +-
 Carleson/ForestOperator/LargeSeparation.lean  |   3 +-
 Carleson/ForestOperator/RemainingTiles.lean   |   3 +-
 Carleson/HardyLittlewood.lean                 |   7 +-
 Carleson/Psi.lean                             |   1 -
 Carleson/RealInterpolation.lean               |  41 +++----
 Carleson/ToMathlib/ENorm.lean                 |  18 +--
 Carleson/ToMathlib/Misc.lean                  |   6 +-
 Carleson/WeakType.lean                        |  13 ++-
 docbuild/lake-manifest.json                   |  34 +++---
 docbuild/lean-toolchain                       |   2 +-
 lake-manifest.json                            | 106 +++++++++---------
 lean-toolchain                                |   2 +-
 18 files changed, 179 insertions(+), 162 deletions(-)

diff --git a/Carleson/Antichain/AntichainOperator.lean b/Carleson/Antichain/AntichainOperator.lean
index dd96d26b..6e0a3865 100644
--- a/Carleson/Antichain/AntichainOperator.lean
+++ b/Carleson/Antichain/AntichainOperator.lean
@@ -54,12 +54,13 @@ open Set Complex MeasureTheory
 -- Lemma 6.1.1
 lemma E_disjoint {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤·) (𝔄 : Set (𝔓 X)))
      {p p' : 𝔓 X} (hp : p ∈ 𝔄) (hp' : p' ∈ 𝔄) (hE : (E p ∩ E p').Nonempty) : p = p' := by
+  wlog h𝔰 : 𝔰 p ≤ 𝔰 p'
+  · have hE' : (E p' ∩ E p).Nonempty := by simp only [inter_comm, hE]
+    symm
+    apply this h𝔄 hp' hp hE' (le_of_lt (not_le.mp h𝔰))
   set x := hE.some
   have hx := hE.some_mem
   simp only [E, mem_inter_iff, mem_setOf_eq] at hx
-  wlog h𝔰 : 𝔰 p ≤ 𝔰 p'
-  · have hE' : (E p' ∩ E p).Nonempty := by simp only [inter_comm, hE]
-    exact eq_comm.mp (this h𝔄 hp' hp hE' hE'.some_mem (le_of_lt (not_le.mp h𝔰)))
   obtain ⟨⟨hx𝓓p, hxΩp, _⟩ , hx𝓓p', hxΩp', _⟩ := hx
   have h𝓓 : 𝓘 p ≤ 𝓘 p' :=
     (or_iff_left (not_disjoint_iff.mpr ⟨x, hx𝓓p, hx𝓓p'⟩)).mp (le_or_disjoint h𝔰)
diff --git a/Carleson/Classical/Approximation.lean b/Carleson/Classical/Approximation.lean
index 7898b1b7..5b5b0e7a 100644
--- a/Carleson/Classical/Approximation.lean
+++ b/Carleson/Classical/Approximation.lean
@@ -12,9 +12,11 @@ open Finset Real
 
 local notation "S_" => partialFourierSum
 
+open scoped ContDiff
+
 lemma close_smooth_approx_periodic {f : ℝ → ℂ} (unicontf : UniformContinuous f)
   (periodicf : f.Periodic (2 * π)) {ε : ℝ} (εpos : ε > 0):
-    ∃ (f₀ : ℝ → ℂ), ContDiff ℝ ⊤ f₀ ∧ f₀.Periodic (2 * π) ∧
+    ∃ (f₀ : ℝ → ℂ), ContDiff ℝ ∞ f₀ ∧ f₀.Periodic (2 * π) ∧
       ∀ x, Complex.abs (f x - f₀ x) ≤ ε := by
   obtain ⟨δ, δpos, hδ⟩ := (Metric.uniformContinuous_iff.mp unicontf) ε εpos
   let φ : ContDiffBump (0 : ℝ) := ⟨δ/2, δ, by linarith, by linarith⟩
@@ -33,7 +35,8 @@ lemma close_smooth_approx_periodic {f : ℝ → ℂ} (unicontf : UniformContinuo
       fun y hy ↦ (hδ hy).le
 
 -- local lemma
-lemma summable_of_le_on_nonzero {f g : ℤ → ℝ} (hgpos : 0 ≤ g) (hgf : ∀ i ≠ 0, g i ≤ f i) (summablef : Summable f) : Summable g := by
+lemma summable_of_le_on_nonzero {f g : ℤ → ℝ} (hgpos : 0 ≤ g) (hgf : ∀ i ≠ 0, g i ≤ f i)
+    (summablef : Summable f) : Summable g := by
   set f' : ℤ → ℝ := fun i ↦ if i = 0 then g i else f i with f'def
   have : ∀ i, g i ≤ f' i := by
     intro i
@@ -114,7 +117,7 @@ lemma fourierCoeffOn_ContDiff_two_bound {f : ℝ → ℂ} (periodicf : f.Periodi
   have h' : ∀ x ∈ Set.uIcc 0 (2 * π), HasDerivAt (deriv f) (deriv (deriv f) x) x := by
     intro x _
     rw [hasDerivAt_deriv_iff]
-    exact (contDiff_succ_iff_deriv.mp fdiff).2.differentiable (by norm_num) _
+    exact ((contDiff_succ_iff_deriv (n := 1)).mp fdiff).2.2.differentiable (by norm_num) _
   /-Get better representation for the fourier coefficients of f. -/
   have fourierCoeffOn_eq {n : ℤ} (hn : n ≠ 0): (fourierCoeffOn Real.two_pi_pos f n) = - 1 / (n^2) * fourierCoeffOn Real.two_pi_pos (fun x ↦ deriv (deriv f) x) n := by
     rw [fourierCoeffOn_of_hasDerivAt Real.two_pi_pos hn h, fourierCoeffOn_of_hasDerivAt Real.two_pi_pos hn h']
@@ -125,9 +128,11 @@ lemma fourierCoeffOn_ContDiff_two_bound {f : ℝ → ℂ} (periodicf : f.Periodi
       simp [h1, h2]
       ring_nf
       simp [mul_inv_cancel, one_mul, pi_pos.ne.symm]
-    · exact (contDiff_one_iff_deriv.mp (contDiff_succ_iff_deriv.mp fdiff).2).2.intervalIntegrable ..
-    · exact (contDiff_succ_iff_deriv.mp fdiff).2.continuous.intervalIntegrable ..
-  obtain ⟨C, hC⟩ := fourierCoeffOn_bound (contDiff_one_iff_deriv.mp (contDiff_succ_iff_deriv.mp fdiff).2).2
+    · exact (contDiff_one_iff_deriv.mp ((contDiff_succ_iff_deriv (n := 1)).mp
+        fdiff).2.2).2.intervalIntegrable ..
+    · exact ((contDiff_succ_iff_deriv (n := 1)).mp fdiff).2.2.continuous.intervalIntegrable ..
+  obtain ⟨C, hC⟩ := fourierCoeffOn_bound (contDiff_one_iff_deriv.mp
+    ((contDiff_succ_iff_deriv (n := 1)).mp fdiff).2.2).2
   refine ⟨C, fun n hn ↦ ?_⟩
   simp only [fourierCoeffOn_eq hn, Nat.cast_one, Int.cast_pow, map_mul, map_div₀, map_neg_eq_map,
   map_one, map_pow, Complex.abs_intCast, sq_abs, one_div, div_eq_mul_inv C, mul_comm _ (Complex.abs _)]
@@ -167,7 +172,8 @@ lemma int_sum_nat {β : Type*} [AddCommGroup β] [TopologicalSpace β] [Continuo
       linarith
 
 
-lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : f.Periodic (2 * π)) (fdiff : ContDiff ℝ 2 f) {ε : ℝ} (εpos : ε > 0) :
+lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : f.Periodic (2 * π))
+    (fdiff : ContDiff ℝ 2 f) {ε : ℝ} (εpos : ε > 0) :
     ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * π), ‖f x - S_ N f x‖ ≤ ε := by
   have fact_two_pi_pos : Fact (0 < 2 * π) := by
     rw [fact_iff]
diff --git a/Carleson/Classical/ClassicalCarleson.lean b/Carleson/Classical/ClassicalCarleson.lean
index 63f7b46a..76a05aed 100644
--- a/Carleson/Classical/ClassicalCarleson.lean
+++ b/Carleson/Classical/ClassicalCarleson.lean
@@ -28,7 +28,7 @@ theorem exceptional_set_carleson {f : ℝ → ℂ}
   obtain ⟨f₀, contDiff_f₀, periodic_f₀, hf₀⟩ := close_smooth_approx_periodic unicont_f periodic_f ε'pos
   have ε4pos : ε / 4 > 0 := by linarith
   obtain ⟨N₀, hN₀⟩ := fourierConv_ofTwiceDifferentiable periodic_f₀
-    ((contDiff_top.mp (contDiff_f₀)) 2) ε4pos
+    ((contDiff_infty.mp (contDiff_f₀)) 2) ε4pos
   set h := f₀ - f with hdef
   have h_measurable : Measurable h := (Continuous.sub contDiff_f₀.continuous cont_f).measurable
   have h_periodic : h.Periodic (2 * π) := periodic_f₀.sub periodic_f
diff --git a/Carleson/Classical/ControlApproximationEffect.lean b/Carleson/Classical/ControlApproximationEffect.lean
index e24e4344..fd7802c1 100644
--- a/Carleson/Classical/ControlApproximationEffect.lean
+++ b/Carleson/Classical/ControlApproximationEffect.lean
@@ -15,9 +15,11 @@ open Real (pi_pos)
 
 
 /- TODO: might be generalized. -/
-lemma ENNReal.le_on_subset {X : Type} [MeasurableSpace X] (μ : Measure X) {f g : X → ENNReal} {E : Set X} (hE : MeasurableSet E)
+lemma ENNReal.le_on_subset {X : Type} [MeasurableSpace X] (μ : Measure X) {f g : X → ENNReal}
+    {E : Set X} (hE : MeasurableSet E)
     (hf : Measurable f) (hg : Measurable g) {a : ENNReal} (h : ∀ x ∈ E, a ≤ f x + g x) :
-    ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E' ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ (∀ x ∈ E', a / 2 ≤ g x)) := by
+    ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E'
+      ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ (∀ x ∈ E', a / 2 ≤ g x)) := by
   set Ef := E ∩ f⁻¹' (Set.Ici (a / 2)) with Ef_def
   set Eg := E ∩ g⁻¹' (Set.Ici (a / 2)) with Eg_def
   have : E ⊆ Ef ∪ Eg := by
@@ -80,11 +82,12 @@ lemma ENNReal.le_on_subset {X : Type} [MeasurableSpace X] (μ : Measure X) {f g
 open Complex ComplexConjugate
 
 lemma Dirichlet_Hilbert_eq {N : ℕ} {x : ℝ} :
-    (max (1 - |x|) 0) * dirichletKernel' N (x) = exp (I * (-N * x)) * k x + conj (exp (I * (-N * x)) * k x) := by
+    (max (1 - |x|) 0) * dirichletKernel' N (x) =
+      exp (I * (-N * x)) * k x + conj (exp (I * (-N * x)) * k x) := by
   simp [dirichletKernel', K, k, conj_ofReal, ←exp_conj, mul_comm, ←mul_assoc, ←exp_add]
   ring_nf
 
-lemma Dirichlet_Hilbert_diff {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc (-π) π):
+lemma Dirichlet_Hilbert_diff {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc (-π) π) :
     ‖dirichletKernel' N (x) - (exp (I * (-N * x)) * k x + conj (exp (I * (-N * x)) * k x))‖ ≤ π := by
   rw [← Dirichlet_Hilbert_eq]
   by_cases h : 1 - cexp (I * ↑x) = 0
@@ -138,11 +141,12 @@ lemma le_iSup_of_tendsto {α β} [TopologicalSpace α] [CompleteLinearOrder α]
     [Nonempty β] [SemilatticeSup β] {f : β → α} {a : α} (ha : Tendsto f atTop (𝓝 a)) : a ≤ iSup f := by
   apply le_of_forall_lt
   intro c hc
-  have : ∀ᶠ (x : β) in atTop, c < f x := eventually_gt_of_tendsto_gt hc ha
+  have : ∀ᶠ (x : β) in atTop, c < f x := Filter.Tendsto.eventually_const_lt hc ha
   rcases this.exists with ⟨x, hx⟩
   exact lt_of_lt_of_le hx (le_iSup _ _)
 
-lemma integrable_annulus {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-π) (3 * π)) {r : ℝ} (r_nonneg : 0 ≤ r) (rle1 : r < 1) :
+lemma integrable_annulus {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) {f : ℝ → ℂ}
+    (hf : IntervalIntegrable f volume (-π) (3 * π)) {r : ℝ} (r_nonneg : 0 ≤ r) (rle1 : r < 1) :
     Integrable (fun x ↦ f x) (volume.restrict {y | dist x y ∈ Set.Ioo r 1}) := by
   rw [← IntegrableOn, annulus_real_eq r_nonneg]
   apply IntegrableOn.union <;>
@@ -152,9 +156,11 @@ lemma integrable_annulus {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) {f : ℝ →
     intro y hy
     constructor <;> linarith [hx.1, hx.2, hy.1, hy.2, Real.two_le_pi]
 
-lemma intervalIntegrable_mul_dirichletKernel' {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-π) (3 * π)) {N : ℕ} :
+lemma intervalIntegrable_mul_dirichletKernel' {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) {f : ℝ → ℂ}
+    (hf : IntervalIntegrable f volume (-π) (3 * π)) {N : ℕ} :
     IntervalIntegrable (fun y ↦ f y * dirichletKernel' N (x - y)) volume (x - π) (x + π) := by
-  apply (hf.mono_set _).mul_bdd (dirichletKernel'_measurable.comp (measurable_id.const_sub _)).aestronglyMeasurable
+  apply (hf.mono_set _).mul_bdd
+    (dirichletKernel'_measurable.comp (measurable_id.const_sub _)).aestronglyMeasurable
   · use (2 * N + 1)
     intro y
     apply norm_dirichletKernel'_le
@@ -162,24 +168,33 @@ lemma intervalIntegrable_mul_dirichletKernel' {x : ℝ} (hx : x ∈ Set.Icc 0 (2
     on_goal 1 => apply Set.Icc_subset_Icc
     all_goals linarith [hx.1, hx.2, pi_pos]
 
-lemma intervalIntegrable_mul_dirichletKernel'_max {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-π) (3 * π)) {N : ℕ} :
-    IntervalIntegrable (fun y ↦ f y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) volume (x - π) (x + π) := by
+lemma intervalIntegrable_mul_dirichletKernel'_max {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) {f : ℝ → ℂ}
+   (hf : IntervalIntegrable f volume (-π) (3 * π)) {N : ℕ} :
+    IntervalIntegrable (fun y ↦ f y * ((max (1 - |x - y|) 0)
+      * dirichletKernel' N (x - y))) volume (x - π) (x + π) := by
   conv => pattern ((f _) * _); rw [← mul_assoc]
-  apply intervalIntegrable_mul_dirichletKernel' hx (IntervalIntegrable.mul_bdd hf (Complex.measurable_ofReal.comp ((Measurable.const_sub (_root_.continuous_abs.measurable.comp (measurable_id.const_sub _)) _).max measurable_const)).aestronglyMeasurable _)
+  apply intervalIntegrable_mul_dirichletKernel' hx
+    (IntervalIntegrable.mul_bdd hf (Complex.measurable_ofReal.comp
+      ((Measurable.const_sub (_root_.continuous_abs.measurable.comp
+        (measurable_id.const_sub _)) _).max measurable_const)).aestronglyMeasurable _)
   use 1
   intro y
   simp only [id_eq, Function.comp_apply, norm_eq_abs, abs_ofReal]
   rw [_root_.abs_of_nonneg (le_max_right _ _)]
   simp
 
-lemma intervalIntegrable_mul_dirichletKernel'_max' {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-π) (3 * π)) {N : ℕ} :
-    IntervalIntegrable (fun y ↦ f y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) volume (x - π) (x + π) := by
+lemma intervalIntegrable_mul_dirichletKernel'_max' {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) {f : ℝ → ℂ}
+    (hf : IntervalIntegrable f volume (-π) (3 * π)) {N : ℕ} :
+    IntervalIntegrable (fun y ↦ f y
+      * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
+      volume (x - π) (x + π) := by
   conv => pattern ((f _) * _); rw [mul_sub]
-  exact (intervalIntegrable_mul_dirichletKernel' hx hf).sub (intervalIntegrable_mul_dirichletKernel'_max hx hf)
+  exact (intervalIntegrable_mul_dirichletKernel' hx hf).sub
+    (intervalIntegrable_mul_dirichletKernel'_max hx hf)
 
-lemma domain_reformulation {g : ℝ → ℂ} (hg : IntervalIntegrable g volume (-π) (3 * π)) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) :
-      ∫ (y : ℝ) in x - π..x + π,
-        g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))
+lemma domain_reformulation {g : ℝ → ℂ} (hg : IntervalIntegrable g volume (-π) (3 * π)) {N : ℕ}
+    {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) :
+    ∫ (y : ℝ) in x - π..x + π, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))
     = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1},
         g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) := by
   calc _
@@ -220,9 +235,13 @@ lemma domain_reformulation {g : ℝ → ℂ} (hg : IntervalIntegrable g volume (
         exact le_trans' (h₀ h₂.1) (by linarith [Real.two_le_pi])
       · trivial
 
-lemma intervalIntegrable_mul_dirichletKernel'_specific {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-π) (3 * π)) {N : ℕ} :
-    IntegrableOn (fun y ↦ f y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) {y | dist x y ∈ Set.Ioo 0 1} volume := by
-  have : IntervalIntegrable (fun y ↦ f y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) volume (x - π) (x + π) := intervalIntegrable_mul_dirichletKernel'_max hx hf
+lemma intervalIntegrable_mul_dirichletKernel'_specific {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π))
+    {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-π) (3 * π)) {N : ℕ} :
+    IntegrableOn (fun y ↦ f y * ((max (1 - |x - y|) 0)
+      * dirichletKernel' N (x - y))) {y | dist x y ∈ Set.Ioo 0 1} volume := by
+  have : IntervalIntegrable (fun y ↦ f y * ((max (1 - |x - y|) 0)
+      * dirichletKernel' N (x - y))) volume (x - π) (x + π) :=
+    intervalIntegrable_mul_dirichletKernel'_max hx hf
   rw [intervalIntegrable_iff_integrableOn_Ioo_of_le (by linarith [pi_pos])] at this
   apply this.mono_set
   intro y hy
@@ -528,7 +547,8 @@ lemma C_control_approximation_effect_eq {ε : ℝ} {δ : ℝ} (ε_nonneg : 0 ≤
 
 /- This is Lemma 11.6.4 (partial Fourier sums of small) in the blueprint.-/
 lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ : 0 < δ)
-    {h : ℝ → ℂ} (h_measurable : Measurable h) (h_periodic : h.Periodic (2 * π)) (h_bound : ∀ x, ‖h x‖ ≤ δ ) :
+    {h : ℝ → ℂ} (h_measurable : Measurable h)
+    (h_periodic : h.Periodic (2 * π)) (h_bound : ∀ x, ‖h x‖ ≤ δ) :
     ∃ E ⊆ Set.Icc 0 (2 * π), MeasurableSet E ∧ volume.real E ≤ ε ∧ ∀ x ∈ Set.Icc 0 (2 * π) \ E,
       ∀ N, ‖S_ N h x‖ ≤ C_control_approximation_effect ε * δ := by
   set ε' := C_control_approximation_effect ε * δ with ε'def
@@ -579,7 +599,7 @@ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ :
       _ = (T h x + T (conj ∘ h) x) + ENNReal.ofReal (π * δ * (2 * π)) := by
         rw [mul_add]
         congr
-        · rw [ENNReal.mul_div_cancel' (by simp [pi_pos]) ENNReal.ofReal_ne_top]
+        · rw [ENNReal.mul_div_cancel (by simp [pi_pos]) ENNReal.ofReal_ne_top]
         · rw [← ENNReal.ofReal_mul Real.two_pi_pos.le]
           ring_nf
   --TODO: align this with paper version
diff --git a/Carleson/Classical/DirichletKernel.lean b/Carleson/Classical/DirichletKernel.lean
index b74976a0..54fa7d53 100644
--- a/Carleson/Classical/DirichletKernel.lean
+++ b/Carleson/Classical/DirichletKernel.lean
@@ -33,6 +33,7 @@ lemma dirichletKernel'_periodic : Function.Periodic (dirichletKernel' N) (2 * π
     congr
     convert exp_int_mul_two_pi_mul_I N using 2
     norm_cast
+    simp
     ring
   · congr 1
     rw [mul_add, exp_add]
@@ -173,7 +174,8 @@ lemma norm_dirichletKernel'_le {x : ℝ} : ‖dirichletKernel' N x‖ ≤ 2 * N
 /-- First part of lemma 11.1.8 (Dirichlet kernel) from the blueprint. -/
 lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {x : ℝ}
     (h : IntervalIntegrable f volume 0 (2 * π)) :
-    partialFourierSum N f x = (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), f y * dirichletKernel N (x - y) := by
+    partialFourierSum N f x =
+      (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), f y * dirichletKernel N (x - y) := by
   calc partialFourierSum N f x
     _ = ∑ n in Icc (-(N : ℤ)) N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x := by
       rw [partialFourierSum]
@@ -204,8 +206,10 @@ lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {x : ℝ}
       field_simp
       rw [mul_sub, sub_eq_neg_add]
 
-lemma partialFourierSum_eq_conv_dirichletKernel' {f : ℝ → ℂ} {x : ℝ} (h : IntervalIntegrable f volume 0 (2 * π)) :
-    partialFourierSum N f x = (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), f y * dirichletKernel' N (x - y) := by
+lemma partialFourierSum_eq_conv_dirichletKernel' {f : ℝ → ℂ} {x : ℝ}
+    (h : IntervalIntegrable f volume 0 (2 * π)) :
+    partialFourierSum N f x =
+      (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), f y * dirichletKernel' N (x - y) := by
   rw [partialFourierSum_eq_conv_dirichletKernel h]
   calc _
     _ = (1 / (2 * π)) * ∫ (y : ℝ) in (x - 2 * π)..(x - 0), f (x - y) * dirichletKernel N y := by
diff --git a/Carleson/Discrete/ForestComplement.lean b/Carleson/Discrete/ForestComplement.lean
index 44cd55c4..7e404df5 100644
--- a/Carleson/Discrete/ForestComplement.lean
+++ b/Carleson/Discrete/ForestComplement.lean
@@ -257,7 +257,7 @@ lemma antichain_decomposition : 𝔓pos (X := X) ∩ 𝔓₁ᶜ = ℜ₀ ∪ ℜ
     simp at h
   contrapose! nG₃
   exact le_iSup₂_of_le n k <| le_iSup₂_of_le hkn j <|
-    le_iSup₂_of_le hj p <| le_iSup_of_le nG₃ subset_rfl
+    le_iSup₂_of_le hj p <| le_iSup_of_le nG₃ Subset.rfl
 
 /-- The subset `𝔏₀(k, n, l)` of `𝔏₀(k, n)`, given in Lemma 5.5.3.
   We use the name `𝔏₀'` in Lean. The indexing is off-by-one w.r.t. the blueprint -/
diff --git a/Carleson/ForestOperator/LargeSeparation.lean b/Carleson/ForestOperator/LargeSeparation.lean
index 701b2180..510e8c8d 100644
--- a/Carleson/ForestOperator/LargeSeparation.lean
+++ b/Carleson/ForestOperator/LargeSeparation.lean
@@ -109,8 +109,7 @@ lemma union_𝓙₅ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u
       contradiction
 
 /-- Part of Lemma 7.5.1. -/
-lemma pairwiseDisjoint_𝓙₅ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂)
-    (h2u : 𝓘 u₁ ≤ 𝓘 u₂) :
+lemma pairwiseDisjoint_𝓙₅ :
     (𝓙₅ t u₁ u₂).PairwiseDisjoint (fun I ↦ (I : Set X)) := by
   have ss : (𝓙 (t.𝔖₀ u₁ u₂) ∩ Iic (𝓘 u₁)) ⊆ 𝓙 (t.𝔖₀ u₁ u₂) := inter_subset_left
   exact PairwiseDisjoint.subset (pairwiseDisjoint_𝓙 (𝔖 := 𝔖₀ t u₁ u₂)) ss
diff --git a/Carleson/ForestOperator/RemainingTiles.lean b/Carleson/ForestOperator/RemainingTiles.lean
index e76e7922..266f8e01 100644
--- a/Carleson/ForestOperator/RemainingTiles.lean
+++ b/Carleson/ForestOperator/RemainingTiles.lean
@@ -111,7 +111,8 @@ lemma square_function_count (hJ : J ∈ 𝓙₆ t u₁) (s' : ℤ) :
     · rw [Finset.mul_sum, ← nsmul_eq_mul, ← Finset.sum_const]
       refine Finset.sum_le_sum fun I hI ↦ ?_
       simp only [mem_toFinset] at hI
-      refine (measureReal_mono ?_ (by finiteness)).trans measure_ball_le_pow_two
+      apply le_trans _ (measure_ball_le_pow_two (μ := volume) (x := c I) (r := D ^ s I / 4))
+      refine measureReal_mono ?_ (by finiteness)
       apply ball_subset_ball'
       refine (add_le_add le_rfl hI.1.le).trans ?_
       rw [div_eq_mul_one_div, mul_comm _ (1 / 4), hI.2, ← add_mul, ← mul_assoc]
diff --git a/Carleson/HardyLittlewood.lean b/Carleson/HardyLittlewood.lean
index 6a8813d8..8391f504 100644
--- a/Carleson/HardyLittlewood.lean
+++ b/Carleson/HardyLittlewood.lean
@@ -166,7 +166,7 @@ theorem exists_disjoint_subfamily_covering_enlargement_closedBall' {α} [MetricS
   push_neg at ht
   let t' := { a ∈ t | 0 ≤ r a }
   have h2τ : 1 < (τ - 1) / 2 := by linarith
-  rcases exists_disjoint_subfamily_covering_enlargment (fun a => closedBall (x a) (r a)) t' r
+  rcases exists_disjoint_subfamily_covering_enlargement (fun a => closedBall (x a) (r a)) t' r
       ((τ - 1) / 2) h2τ (fun a ha => ha.2) R (fun a ha => hr a ha.1) fun a ha =>
       ⟨x a, mem_closedBall_self ha.2⟩ with
     ⟨u, ut', u_disj, hu⟩
@@ -289,7 +289,7 @@ protected theorem HasStrongType.MB_top [BorelSpace X] (h𝓑 : 𝓑.Countable) :
   use AEStronglyMeasurable.maximalFunction_toReal h𝓑
   simp only [ENNReal.coe_one, one_mul, eLpNorm_exponent_top]
   refine essSup_le_of_ae_le _ (Eventually.of_forall fun x ↦ ?_)
-  simp_rw [ENNReal.nnorm_toReal]
+  simp_rw [enorm_eq_nnnorm, ENNReal.nnorm_toReal]
   exact ENNReal.coe_toNNReal_le_self |>.trans MB_le_eLpNormEssSup
 
 protected theorem MeasureTheory.AESublinearOn.maximalFunction
@@ -462,7 +462,8 @@ def C2_0_6' (A p₁ p₂ : ℝ≥0) : ℝ≥0 := A ^ 2 * C2_0_6 A p₁ p₂
 /-- Equation (2.0.46).
 Easy from `hasStrongType_maximalFunction`. Ideally prove separately
 `HasStrongType.const_smul` and `HasStrongType.const_mul`. -/
-theorem hasStrongType_globalMaximalFunction [BorelSpace X] [IsFiniteMeasureOnCompacts μ] [Nonempty X] [μ.IsOpenPosMeasure] {p₁ p₂ : ℝ≥0} (hp₁ : 1 ≤ p₁) (hp₁₂ : p₁ < p₂) :
+theorem hasStrongType_globalMaximalFunction [BorelSpace X] [IsFiniteMeasureOnCompacts μ]
+    [Nonempty X] [μ.IsOpenPosMeasure] {p₁ p₂ : ℝ≥0} (hp₁ : 1 ≤ p₁) (hp₁₂ : p₁ < p₂) :
     HasStrongType (fun (u : X → E) (x : X) ↦ globalMaximalFunction μ p₁ u x |>.toReal)
       p₂ p₂ μ μ (C2_0_6' A p₁ p₂) := by
   -- unfold globalMaximalFunction
diff --git a/Carleson/Psi.lean b/Carleson/Psi.lean
index fe835c31..dfc78542 100644
--- a/Carleson/Psi.lean
+++ b/Carleson/Psi.lean
@@ -1,6 +1,5 @@
 import Carleson.Defs
 import Mathlib.Algebra.Lie.OfAssociative
-import Mathlib.Topology.CompletelyRegular
 import Mathlib.Topology.EMetricSpace.Paracompact
 
 open MeasureTheory Measure NNReal Metric Set TopologicalSpace Function DoublingMeasure Bornology
diff --git a/Carleson/RealInterpolation.lean b/Carleson/RealInterpolation.lean
index 0183ef84..ba8a3b68 100644
--- a/Carleson/RealInterpolation.lean
+++ b/Carleson/RealInterpolation.lean
@@ -7,7 +7,7 @@ import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
     follow the technique as e.g. described in [Duoandikoetxea, Fourier Analysis, 2000].
 
     The file consists of the following sections:
-    - Convience results for working with (interpolated) exponents
+    - Convenience results for working with (interpolated) exponents
     - Results about the particular choice of exponent
     - Interface for using cutoff functions
     - Results about the particular choice of scale
@@ -23,8 +23,6 @@ import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
     - Proof of the real interpolation theorem
 -/
 
-set_option linter.unusedVariables false -- contrapose! is noisy
-
 noncomputable section
 
 open ENNReal Real Set MeasureTheory
@@ -1508,7 +1506,7 @@ lemma coe_coe_eq_ofReal (a : ℝ) : ofNNReal a.toNNReal = ENNReal.ofReal a := by
 lemma trunc_eLpNormEssSup_le {f : α → E₁} {a : ℝ} [NormedAddCommGroup E₁] :
     eLpNormEssSup (trunc f a) μ ≤ ENNReal.ofReal (max 0 a) := by
   refine essSup_le_of_ae_le _ (ae_of_all _ fun x ↦ ?_)
-  simp only [← norm_toNNReal, coe_coe_eq_ofReal]
+  simp only [enorm_eq_nnnorm, ← norm_toNNReal, coe_coe_eq_ofReal]
   exact ofReal_le_ofReal (trunc_le x)
 
 lemma trunc_mono {f : α → E₁} {a b : ℝ} [NormedAddCommGroup E₁]
@@ -1523,7 +1521,7 @@ lemma trunc_mono {f : α → E₁} {a b : ℝ} [NormedAddCommGroup E₁]
 /-- The norm of the truncation is monotone in the truncation parameter -/
 lemma norm_trunc_mono {f : α → E₁} [NormedAddCommGroup E₁] :
     Monotone fun s ↦ eLpNorm (trunc f s) p μ :=
-  fun a b hab ↦ eLpNorm_mono fun x ↦ trunc_mono hab
+  fun _a _b hab ↦ eLpNorm_mono fun _x ↦ trunc_mono hab
 
 lemma trunc_buildup_norm {f : α → E₁} {a : ℝ} {x : α} [NormedAddCommGroup E₁] :
     ‖trunc f a x‖ + ‖(f - trunc f a) x‖ = ‖f x‖ := by
@@ -1658,7 +1656,7 @@ lemma estimate_eLpNorm_trunc_compl {p q : ℝ≥0∞} [MeasurableSpace E₁] [No
   split_ifs
   · contradiction
   · calc
-    _ = ∫⁻ x : α in {x | a < ‖f x‖}, ↑‖(f - trunc f a) x‖₊ ^ q.toReal ∂μ := by
+    _ = ∫⁻ x : α in {x | a < ‖f x‖}, ‖(f - trunc f a) x‖ₑ ^ q.toReal ∂μ := by
       rw [one_div, ENNReal.rpow_inv_rpow]
       · apply (setLIntegral_eq_of_support_subset _).symm
         unfold Function.support
@@ -1667,19 +1665,20 @@ lemma estimate_eLpNorm_trunc_compl {p q : ℝ≥0∞} [MeasurableSpace E₁] [No
         dsimp only [Pi.sub_apply, mem_setOf_eq]
         split_ifs with is_a_lt_fx
         · exact fun _ => is_a_lt_fx
-        · contrapose; intro _; simpa
+        · contrapose; intro _; simpa [enorm_eq_nnnorm]
       · exact exp_toReal_ne_zero' hpq.1 q_ne_top
-    _ ≤ ∫⁻ x : α in {x | a < ‖f x‖}, ↑‖f x‖₊ ^ q.toReal ∂μ := by
+    _ ≤ ∫⁻ x : α in {x | a < ‖f x‖}, ‖f x‖ₑ ^ q.toReal ∂μ := by
       apply lintegral_mono_ae
       apply ae_of_all
       intro x
       gcongr
-      rw [← norm_toNNReal, ← norm_toNNReal]
-      apply Real.toNNReal_mono
+      rw [enorm_eq_nnnorm, ← norm_toNNReal, enorm_eq_nnnorm, ← norm_toNNReal]
+      simp only [Pi.sub_apply, ENNReal.coe_le_coe, norm_nonneg, Real.toNNReal_le_toNNReal_iff]
       apply trnc_le_func (j := ⊥)
     _ ≤ ENNReal.ofReal (a ^ (q.toReal - p.toReal)) * ∫⁻ x : α in {x | a < ‖f x‖},
-        ↑‖f x‖₊ ^ p.toReal ∂μ := by
+        ‖f x‖ₑ ^ p.toReal ∂μ := by
       rw [← lintegral_const_mul']; swap; · exact coe_ne_top
+      simp only [enorm_eq_nnnorm]
       apply setLIntegral_mono_ae (AEMeasurable.restrict (by fun_prop))
       · apply ae_of_all
         intro x (hx : a < ‖f x‖)
@@ -1694,7 +1693,8 @@ lemma estimate_eLpNorm_trunc_compl {p q : ℝ≥0∞} [MeasurableSpace E₁] [No
       exact setLIntegral_le_lintegral _ _
     _ = _ := by
       rw [one_div, ENNReal.rpow_inv_rpow]
-      refine exp_toReal_ne_zero' (lt_trans hpq.1 hpq.2) hp
+      · simp only [enorm_eq_nnnorm]
+      · exact exp_toReal_ne_zero' (lt_trans hpq.1 hpq.2) hp
 
 lemma estimate_eLpNorm_trunc {p q : ℝ≥0∞}
     [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁]
@@ -1869,14 +1869,14 @@ lemma lintegral_trunc_mul₀ {g : ℝ → ℝ≥0∞} {j : Bool} {x : α} {tc :
       split_ifs at mon_pf with mon
       · rw [mon]
         rcases j
-        · simp only [Bool.bne_true, Bool.not_false, not_true_eq_false, decide_False,
+        · simp only [Bool.bne_true, Bool.not_false, not_true_eq_false, decide_false,
           Bool.false_eq_true, ↓reduceIte, Pi.sub_apply]
           intro (hs : s > tc.inv ‖f x‖)
           split_ifs with h
           · simp [hp]
           · have := (mon_pf s (lt_trans (tc.ran_inv ‖f x‖ hfx) hs) (‖f x‖) hfx).2.mpr hs
             contrapose! h; linarith
-        · simp only [bne_self_eq_false, Bool.false_eq_true, not_false_eq_true, decide_True]
+        · simp only [bne_self_eq_false, Bool.false_eq_true, not_false_eq_true, decide_true]
           intro hs
           split_ifs with h
           · have := (mon_pf s hs.1 (‖f x‖) hfx).1.mpr hs.2
@@ -1885,14 +1885,14 @@ lemma lintegral_trunc_mul₀ {g : ℝ → ℝ≥0∞} {j : Bool} {x : α} {tc :
       · rw [Bool.not_eq_true] at mon
         rw [mon]
         rcases j
-        · simp only [bne_self_eq_false, Bool.false_eq_true, not_false_eq_true, decide_True,
+        · simp only [bne_self_eq_false, Bool.false_eq_true, not_false_eq_true, decide_true,
           ↓reduceIte, Pi.sub_apply]
           intro hs
           split_ifs with h
           · simp [hp]
           · have := (mon_pf s hs.1 (‖f x‖) hfx).2.mpr hs.2
             linarith
-        · simp only [Bool.bne_false, not_true_eq_false, decide_False, Bool.false_eq_true, ↓reduceIte]
+        · simp only [Bool.bne_false, not_true_eq_false, decide_false, Bool.false_eq_true, ↓reduceIte]
           intro (hs : tc.inv ‖f x‖ < s)
           have := (mon_pf s (lt_trans (tc.ran_inv ‖f x‖ hfx) hs) (‖f x‖) hfx).1.mpr hs
           split_ifs with h
@@ -2500,6 +2500,7 @@ lemma estimate_trnc {p₀ q₀ q : ℝ} {spf : ScaledPowerFunction} {j : Bool}
     calc
     _ = ∫⁻ s : ℝ in Ioi 0, ENNReal.ofReal (s ^ (q - q₀ - 1)) *
     ((∫⁻ (a : α), ↑‖trnc j f ((spf_to_tc spf).ton s) a‖₊ ^ p₀ ∂μ) ^ (1 / p₀)) ^ q₀  := by
+      simp only [enorm_eq_nnnorm]
       congr 1
       ext x
       rw [mul_comm]
@@ -2559,7 +2560,7 @@ lemma estimate_trnc {p₀ q₀ q : ℝ} {spf : ScaledPowerFunction} {j : Bool}
       congr 2
       · apply value_lintegral_res₀
         · apply tc.ran_inv
-          exact norm_pos_iff'.mpr hfx
+          exact norm_pos_iff.mpr hfx
         · split_ifs with h
           · simp only [h, ↓reduceIte] at hpowers; linarith
           · simp only [h, Bool.false_eq_true, ↓reduceIte] at hpowers; linarith
@@ -2575,7 +2576,7 @@ lemma estimate_trnc {p₀ q₀ q : ℝ} {spf : ScaledPowerFunction} {j : Bool}
       intro x hfx
       congr 1
       apply value_lintegral_res₁
-      exact norm_pos_iff'.mpr hfx
+      exact norm_pos_iff.mpr hfx
     _ = (∫⁻ a : α in Function.support f,
         ((ENNReal.ofReal (spf.d ^ (q - q₀)) ^ (p₀⁻¹ * q₀)⁻¹ *
         ENNReal.ofReal (‖f a‖ ^ ((spf.σ⁻¹ * (q - q₀) + q₀) * (p₀⁻¹ * q₀)⁻¹)) *
@@ -3211,6 +3212,7 @@ lemma rewrite_norm_func {q : ℝ} {g : α' → E}
     ∫⁻ x, ‖g x‖₊ ^q ∂ν =
     ENNReal.ofReal ((2 * A)^q * q) * ∫⁻ s in Ioi (0 : ℝ),
     distribution g ((ENNReal.ofReal (2 * A * s)))  ν * (ENNReal.ofReal (s^(q - 1))) := by
+  simp only [← enorm_eq_nnnorm]
   rw [lintegral_norm_pow_eq_distribution hg (by linarith)]
   nth_rewrite 1 [← lintegral_scale_constant_halfspace' (a := (2*A)) (by linarith)]
   rw [← lintegral_const_mul']; swap; · exact coe_ne_top
@@ -3246,7 +3248,7 @@ lemma estimate_norm_rpow_range_operator {q : ℝ} {f : α → E₁}
 
 -- XXX: can this be golfed or unified with `ton_aeMeasurable`?
 @[measurability, fun_prop]
-theorem ton_aeMeasurable_eLpNorm_trunc [MeasurableSpace E₁] [NormedAddCommGroup E₁] (tc : ToneCouple) :
+theorem ton_aeMeasurable_eLpNorm_trunc [NormedAddCommGroup E₁] (tc : ToneCouple) :
     AEMeasurable (fun x ↦ eLpNorm (trunc f (tc.ton x)) p₁ μ) (volume.restrict (Ioi 0)) := by
   change AEMeasurable ((fun t : ℝ ↦ eLpNorm (trunc f t) p₁ μ) ∘ (tc.ton)) (volume.restrict (Ioi 0))
   have tone := tc.ton_is_ton
@@ -3710,6 +3712,7 @@ lemma combine_estimates₁ {A : ℝ} [MeasurableSpace E₁] [NormedAddCommGroup
   calc
   _ = ∫⁻ x , ‖T f x‖₊ ^ q.toReal ∂ν := by
     unfold eLpNorm eLpNorm'
+    simp only [← enorm_eq_nnnorm]
     split_ifs <;> [contradiction; rw [one_div, ENNReal.rpow_inv_rpow q'pos.ne']]
   _ ≤ _ := by
     apply combine_estimates₀ (hT := hT) (p := p) <;> try assumption
diff --git a/Carleson/ToMathlib/ENorm.lean b/Carleson/ToMathlib/ENorm.lean
index fa9a936e..1911ba2c 100644
--- a/Carleson/ToMathlib/ENorm.lean
+++ b/Carleson/ToMathlib/ENorm.lean
@@ -11,17 +11,6 @@ noncomputable section
 
 open ENNReal NNReal MeasureTheory Function Set
 
-/-- Auxiliary class, endowing a type `α` with a function `enorm : α → ℝ≥0∞` with notation `‖x‖ₑ`. -/
-@[notation_class]
-class ENorm (E : Type*) where
-  /-- the `ℝ≥0∞`-valued norm function. -/
-  enorm : E → ℝ≥0∞
-
-export ENorm (enorm)
-
-@[inherit_doc]
-notation "‖" e "‖ₑ" => enorm e
-
 /-- An enormed monoid is an additive monoid endowed with an enorm. -/
 class ENormedAddMonoid (E : Type*) extends ENorm E, AddMonoid E, TopologicalSpace E where
   enorm_zero : ∀ x : E, enorm x = 0 ↔ x = 0
@@ -42,11 +31,6 @@ instance : ENormedAddCommMonoid ℝ≥0∞ where
   enorm_triangle := by simp
   add_comm := by simp [add_comm]
 
-instance [NNNorm E] : ENorm E where
-  enorm := (‖·‖₊ : E → ℝ≥0∞)
-
-lemma enorm_eq_nnnorm [NNNorm E] {x : E} : ‖x‖ₑ = ‖x‖₊ := rfl
-
 instance [NormedAddGroup E] : ENormedAddMonoid E where
   enorm_zero := by simp [enorm_eq_nnnorm]
   enorm_neg := by
@@ -284,7 +268,7 @@ theorem exists_disjoint_subfamily_covering_enlargement_closedBall' {α} [MetricS
   push_neg at ht
   let t' := { a ∈ t | 0 ≤ r a }
   have h2τ : 1 < (τ - 1) / 2 := by linarith
-  rcases exists_disjoint_subfamily_covering_enlargment (fun a => closedBall (x a) (r a)) t' r
+  rcases exists_disjoint_subfamily_covering_enlargement (fun a => closedBall (x a) (r a)) t' r
       ((τ - 1) / 2) h2τ (fun a ha => ha.2) R (fun a ha => hr a ha.1) fun a ha =>
       ⟨x a, mem_closedBall_self ha.2⟩ with
     ⟨u, ut', u_disj, hu⟩
diff --git a/Carleson/ToMathlib/Misc.lean b/Carleson/ToMathlib/Misc.lean
index 1887d2a1..f2806cdd 100644
--- a/Carleson/ToMathlib/Misc.lean
+++ b/Carleson/ToMathlib/Misc.lean
@@ -53,15 +53,11 @@ lemma tsum_one_eq' {α : Type*} (s : Set α) : ∑' (_:s), (1 : ℝ≥0∞) = s.
   rw [Set.encard_eq_top_iff.mpr hfin]
   simp only [ENat.toENNReal_top]
 
-#find_home! tsum_one_eq'
-
 lemma ENNReal.tsum_const_eq' {α : Type*} (s : Set α) (c : ℝ≥0∞) :
     ∑' (_:s), (c : ℝ≥0∞) = s.encard * c := by
   nth_rw 1 [← one_mul c]
   rw [ENNReal.tsum_mul_right,tsum_one_eq']
 
-#find_home! ENNReal.tsum_const_eq'
-
 /-! ## `ENNReal` manipulation lemmas -/
 
 lemma ENNReal.sum_geometric_two_pow_toNNReal {k : ℕ} (hk : k > 0) :
@@ -319,7 +315,7 @@ lemma Real.self_lt_two_rpow (x : ℝ) : x < 2 ^ x := by
   · exact h.trans (rpow_pos_of_pos zero_lt_two x)
   · calc
       _ < (⌊x⌋₊.succ : ℝ) := Nat.lt_succ_floor x
-      _ ≤ 2 ^ (⌊x⌋₊ : ℝ) := by exact_mod_cast Nat.lt_pow_self one_lt_two _
+      _ ≤ 2 ^ (⌊x⌋₊ : ℝ) := by exact_mod_cast Nat.lt_pow_self one_lt_two
       _ ≤ _ := rpow_le_rpow_of_exponent_le one_le_two (Nat.floor_le h)
 
 namespace Set
diff --git a/Carleson/WeakType.lean b/Carleson/WeakType.lean
index b886c9d6..689cc8da 100644
--- a/Carleson/WeakType.lean
+++ b/Carleson/WeakType.lean
@@ -22,7 +22,7 @@ variable {α α' 𝕜 E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {m : Me
 -- #check meas_ge_le_mul_pow_eLpNorm -- Chebyshev's inequality
 
 namespace MeasureTheory
-/- If we need more properties of `E`, we can add `[RCLike E]` *instead of* the above type-classes-/
+/- If we need more properties of `E`, we can add `[RCLike 𝕜]` *instead of* the above type-classes-/
 -- #check _root_.RCLike
 
 /- Proofs for this file can be found in
@@ -232,9 +232,11 @@ lemma _root_.ContinuousLinearMap.distribution_le {f : α → E₁} {g : α → E
     calc
       (‖(L (f z)) (g z)‖₊ : ℝ≥0∞) ≤ ‖L‖₊ * ‖f z‖₊ * ‖g z‖₊ := by
         refine (toNNReal_le_toNNReal coe_ne_top coe_ne_top).mp ?_
+        simp only [toNNReal_coe, coe_mul, toNNReal_mul]
         calc
           _ ≤ ↑‖L (f z)‖₊ * ↑‖g z‖₊ := ContinuousLinearMap.le_opNNNorm (L (f z)) (g z)
-          _ ≤ _ := mul_le_mul' (ContinuousLinearMap.le_opNNNorm L (f z)) (by rfl)
+          _ ≤ ‖L‖₊ * ‖f z‖₊ * ‖g z‖₊ :=
+            mul_le_mul' (ContinuousLinearMap.le_opNNNorm L (f z)) (by rfl)
       _ ≤ _ := mul_le_mul' (mul_le_mul_left' hz.1 ↑‖L‖₊) hz.2
   calc
     _ ≤ μ ({x | t < ↑‖f x‖₊} ∪ {x | s < ↑‖g x‖₊}) := measure_mono h₀
@@ -257,7 +259,7 @@ include hf
 
 /-- The layer-cake theorem, or Cavalieri's principle for functions into a normed group. -/
 lemma lintegral_norm_pow_eq_distribution {p : ℝ} (hp : 0 < p) :
-    ∫⁻ x, ‖f x‖₊ ^ p ∂μ =
+    ∫⁻ x, ‖f x‖ₑ ^ p ∂μ =
     ∫⁻ t in Ioi (0 : ℝ), ENNReal.ofReal (p * t ^ (p - 1)) * distribution f (.ofReal t) μ := by
   have h2p : 0 ≤ p := hp.le
   have := lintegral_rpow_eq_lintegral_meas_lt_mul μ (f := fun x ↦ ‖f x‖)
@@ -266,6 +268,7 @@ lemma lintegral_norm_pow_eq_distribution {p : ℝ} (hp : 0 < p) :
     not_false_eq_true, ← lintegral_const_mul', ← mul_assoc, ← ofReal_norm_eq_coe_nnnorm, ofReal_mul,
     distribution, h2p] at this ⊢
   convert this using 1
+  · simp [ENNReal.ofReal, enorm_eq_nnnorm, norm_toNNReal]
   refine setLIntegral_congr_fun measurableSet_Ioi (Eventually.of_forall fun x hx ↦ ?_)
   simp_rw [ENNReal.ofReal_lt_ofReal_iff_of_nonneg (le_of_lt hx)]
 
@@ -298,7 +301,7 @@ lemma eLpNorm_eq_distribution {p : ℝ} (hp : 0 < p) :
 
 lemma lintegral_pow_mul_distribution {p : ℝ} (hp : -1 < p) :
     ∫⁻ t in Ioi (0 : ℝ), ENNReal.ofReal (t ^ p) * distribution f (.ofReal t) μ =
-    ENNReal.ofReal (p + 1)⁻¹ * ∫⁻ x, ‖f x‖₊ ^ (p + 1) ∂μ := by
+    ENNReal.ofReal (p + 1)⁻¹ * ∫⁻ x, ‖f x‖ₑ ^ (p + 1) ∂μ := by
   have h2p : 0 < p + 1 := by linarith
   have h3p : 0 ≤ p + 1 := by linarith
   have h4p : p + 1 ≠ 0 := by linarith
@@ -383,7 +386,7 @@ lemma HasStrongType.const_smul {𝕜 E E' α α' : Type*} [NormedAddCommGroup E]
     [NormedRing 𝕜] [MulActionWithZero 𝕜 E'] [BoundedSMul 𝕜 E'] (k : 𝕜) :
     HasStrongType (k • T) p p' μ ν (‖k‖₊ * c) := by
   refine fun f hf ↦
-    ⟨AEStronglyMeasurable.const_smul (h f hf).1 k, (eLpNorm_const_smul_le k (T f)).trans ?_⟩
+    ⟨AEStronglyMeasurable.const_smul (h f hf).1 k, eLpNorm_const_smul_le.trans ?_⟩
   simp only [ENNReal.smul_def, smul_eq_mul, coe_mul, mul_assoc]
   gcongr
   exact (h f hf).2
diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json
index 81bc9720..b22425ad 100644
--- a/docbuild/lake-manifest.json
+++ b/docbuild/lake-manifest.json
@@ -5,47 +5,47 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a822446d61ad7e7f5e843365c7041c326553050a",
+   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
+   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.15.0",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "de91b59101763419997026c35a41432ac8691f15",
+   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
+   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.46",
+   "inputRev": "v0.0.48",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "119b022b3ea88ec810a677888528e50f8144a26e",
+   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,17 +75,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
+   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "840e02ce2768e06de7ced0a624444746590e9d99",
+   "rev": "e71f6e9769283aa927ec7842e7e75e45f6f30324",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "11fa569b1b52f987dc5dcea97fd80eaff95c2fce",
+   "rev": "75d7aea6c81efeb68701164edaaa9116f06b91ba",
    "name": "checkdecls",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
diff --git a/docbuild/lean-toolchain b/docbuild/lean-toolchain
index 57a4710c..d0eb99ff 100644
--- a/docbuild/lean-toolchain
+++ b/docbuild/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc2
+leanprover/lean4:v4.15.0
diff --git a/lake-manifest.json b/lake-manifest.json
index 143f7f19..386e64de 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,105 +1,105 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/PatrickMassot/checkdecls.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "75d7aea6c81efeb68701164edaaa9116f06b91ba",
+   "name": "checkdecls",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "e71f6e9769283aa927ec7842e7e75e45f6f30324",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a822446d61ad7e7f5e843365c7041c326553050a",
-   "name": "batteries",
+   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
+   "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/quote4",
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
-   "name": "Qq",
+   "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
+   "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "de91b59101763419997026c35a41432ac8691f15",
-   "name": "aesop",
+   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
+   "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
+   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.46",
+   "inputRev": "v0.0.48",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover",
-   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
-   "name": "Cli",
+   "scope": "leanprover-community",
+   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/import-graph",
+  {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "119b022b3ea88ec810a677888528e50f8144a26e",
-   "name": "importGraph",
+   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
+   "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
-   "name": "LeanSearchClient",
+   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/plausible",
+  {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
-   "name": "plausible",
+   "scope": "leanprover",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
+   "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "840e02ce2768e06de7ced0a624444746590e9d99",
-   "name": "mathlib",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": null,
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/PatrickMassot/checkdecls.git",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "11fa569b1b52f987dc5dcea97fd80eaff95c2fce",
-   "name": "checkdecls",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.toml"}],
  "name": "carleson",
  "lakeDir": ".lake"}
diff --git a/lean-toolchain b/lean-toolchain
index 57a4710c..d0eb99ff 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc2
+leanprover/lean4:v4.15.0