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 <[email protected]>
fpvandoorn · Jan 6, 2025 · 386a3c6 · 386a3c6
1 parent 6a0e16d
commit 386a3c6
Show file tree

Hide file tree

Showing 18 changed files with 179 additions and 162 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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,34 +156,45 @@ 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
   · rw [Set.uIcc_of_le, Set.uIcc_of_le]
     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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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