From 01189dc6e085c25e67d422b89d0cfa9e18933d8d Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Tue, 10 Sep 2024 00:23:37 +0400
Subject: [PATCH] Cleanup and Section 7.2 (#118)

* Cleanup some imports
* Cleanup some `Real.pi`
* Use notation for `Finset.univ.filter`
* State lemmas in Section 7.2
---
 CONTRIBUTING.md                               |   6 +-
 Carleson/Classical/Approximation.lean         |  62 +++---
 Carleson/Classical/Basic.lean                 |  73 ++++---
 Carleson/Classical/CarlesonOnTheRealLine.lean |  13 +-
 Carleson/Classical/ClassicalCarleson.lean     |  22 +-
 .../Classical/ControlApproximationEffect.lean | 204 +++++++++---------
 Carleson/Classical/DirichletKernel.lean       |  39 ++--
 Carleson/Classical/HilbertKernel.lean         |   9 +-
 Carleson/Classical/VanDerCorput.lean          |  97 ++++-----
 Carleson/Discrete/Defs.lean                   |   4 +-
 Carleson/Discrete/ExceptionalSet.lean         |  24 +--
 Carleson/Discrete/Forests.lean                |  12 +-
 Carleson/FinitaryCarleson.lean                |   4 +-
 Carleson/Forest.lean                          |   4 +-
 Carleson/ForestOperator.lean                  |  60 ++++--
 Carleson/GridStructure.lean                   |   2 +-
 blueprint/src/chapter/main.tex                |  10 +-
 17 files changed, 336 insertions(+), 309 deletions(-)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index cde2f7c2..5ead4932 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -35,7 +35,7 @@ Below, I will try to give a translation of some notation/conventions. We use mat
 | `T_Q^θ f(x)`       | `linearizedNontangentialOperator Q θ K f x`       | The linearized associated nontangential Calderon Zygmund operator |
 | `T f(x)`       | `carlesonOperator K f x` | The generalized Carleson operator        |
 | `T_Q f(x)`       | `linearizedCarlesonOperator Q K f x` | The linearized generalized Carleson operator        |
-| `T_𝓝^θ f(x)`       | `nontangentialMaximalFunction K θ f x` |   |
+| `T_𝓝^θ f(x)`       | `nontangentialMaximalFunction θ f x` |   |
 | `Tₚ f(x)`       | `carlesonOn p f x`       |         |
 | `e(x)`       | `Complex.exp (Complex.I * x)` |         |
 | `𝔓(I)`       | `𝓘 ⁻¹' {I}` |         |
@@ -48,8 +48,8 @@ Below, I will try to give a translation of some notation/conventions. We use mat
 | `M`        | `globalMaximalFunction volume 1` |     |
 | `I_i(x)`        | `cubeOf i x` |     |
 | `R_Q(θ, x)`        | `upperRadius Q θ x` |     |
-| `S_{1,𝔲} f(x)`        | `auxiliaryOperator1 u f x` |     |
-| `S_{2,𝔲} g(x)`        | `auxiliaryOperator2 u g x` |     |
+| `S_{1,𝔲} f(x)`        | `boundaryOperator1 t u f x` |     |
+| `S_{2,𝔲} g(x)`        | `boundaryOperator2 t u g x` |     |
 | ``        | `` |     |
 | ``        | `` |     |
 | ``        | `` |     |
diff --git a/Carleson/Classical/Approximation.lean b/Carleson/Classical/Approximation.lean
index 8dffe733..a680622d 100644
--- a/Carleson/Classical/Approximation.lean
+++ b/Carleson/Classical/Approximation.lean
@@ -1,25 +1,21 @@
 /- This file contains the arguments from section 11.2 (smooth functions) from the blueprint. -/
 
-import Carleson.MetricCarleson
 import Carleson.Classical.Basic
 
-import Mathlib.Analysis.Fourier.AddCircle
-import Mathlib.Analysis.Convolution
 import Mathlib.Analysis.Calculus.BumpFunction.Convolution
 import Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
 import Mathlib.Analysis.PSeries
 
 noncomputable section
 
-open BigOperators
-open Finset
+open BigOperators Finset Real
 
 local notation "S_" => partialFourierSum
 
 
 lemma close_smooth_approx_periodic {f : ℝ → ℂ} (unicontf : UniformContinuous f)
-  (periodicf : f.Periodic (2 * Real.pi)) {ε : ℝ} (εpos : ε > 0):
-    ∃ (f₀ : ℝ → ℂ), ContDiff ℝ ⊤ f₀ ∧ f₀.Periodic (2 * Real.pi) ∧
+  (periodicf : f.Periodic (2 * π)) {ε : ℝ} (εpos : ε > 0):
+    ∃ (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⟩
@@ -55,8 +51,8 @@ lemma summable_of_le_on_nonzero {f g : ℤ → ℝ} (hgpos : 0 ≤ g) (hgf : ∀
   rw [mem_singleton] at hb
   exact if_neg hb
 
-lemma continuous_bounded {f : ℝ → ℂ} (hf : ContinuousOn f (Set.Icc 0 (2 * Real.pi))) : ∃ C, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x) ≤ C := by
-  have interval_compact := (isCompact_Icc (a := 0) (b := 2 * Real.pi))
+lemma continuous_bounded {f : ℝ → ℂ} (hf : ContinuousOn f (Set.Icc 0 (2 * π))) : ∃ C, ∀ x ∈ Set.Icc 0 (2 * π), Complex.abs (f x) ≤ C := by
+  have interval_compact := (isCompact_Icc (a := 0) (b := 2 * π))
   obtain ⟨a, _, ha⟩ := interval_compact.exists_isMaxOn (Set.nonempty_Icc.mpr Real.two_pi_pos.le)
     (Complex.continuous_abs.comp_continuousOn hf)
   refine ⟨Complex.abs (f a), fun x hx ↦ ?_⟩
@@ -72,31 +68,31 @@ lemma fourierCoeffOn_bound {f : ℝ → ℂ} (f_continuous : Continuous f) : ∃
     fourier_coe_apply', Complex.ofReal_mul, Complex.ofReal_ofNat, smul_eq_mul, Complex.real_smul,
     Complex.ofReal_inv, map_mul, map_inv₀, Complex.abs_ofReal, Complex.abs_ofNat]
   field_simp
-  rw [abs_of_nonneg Real.pi_pos.le, mul_comm Real.pi, div_le_iff₀ Real.two_pi_pos, ←Complex.norm_eq_abs]
-  calc ‖∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), (starRingEnd ℂ) (Complex.exp (2 * Real.pi * Complex.I * n * x / (2 * Real.pi))) * f x‖
-    _ = ‖∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), (starRingEnd ℂ) (Complex.exp (Complex.I * n * x)) * f x‖ := by
+  rw [abs_of_nonneg pi_pos.le, mul_comm π, div_le_iff₀ Real.two_pi_pos, ←Complex.norm_eq_abs]
+  calc ‖∫ (x : ℝ) in (0 : ℝ)..(2 * π), (starRingEnd ℂ) (Complex.exp (2 * π * Complex.I * n * x / (2 * π))) * f x‖
+    _ = ‖∫ (x : ℝ) in (0 : ℝ)..(2 * π), (starRingEnd ℂ) (Complex.exp (Complex.I * n * x)) * f x‖ := by
       congr with x
       congr
       ring_nf
       rw [mul_comm, ←mul_assoc, ←mul_assoc, ←mul_assoc, inv_mul_cancel₀]
       · ring
-      · simp [ne_eq, Complex.ofReal_eq_zero, Real.pi_pos.ne.symm]
-    _ ≤ ∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), ‖(starRingEnd ℂ) (Complex.exp (Complex.I * n * x)) * f x‖ := by
+      · simp [ne_eq, Complex.ofReal_eq_zero, pi_pos.ne.symm]
+    _ ≤ ∫ (x : ℝ) in (0 : ℝ)..(2 * π), ‖(starRingEnd ℂ) (Complex.exp (Complex.I * n * x)) * f x‖ := by
       exact intervalIntegral.norm_integral_le_integral_norm Real.two_pi_pos.le
-    _ = ∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), ‖(Complex.exp (Complex.I * n * x)) * f x‖ := by
+    _ = ∫ (x : ℝ) in (0 : ℝ)..(2 * π), ‖(Complex.exp (Complex.I * n * x)) * f x‖ := by
       simp
-    _ = ∫ (x : ℝ) in (0 : ℝ)..(2 * Real.pi), ‖f x‖ := by
+    _ = ∫ (x : ℝ) in (0 : ℝ)..(2 * π), ‖f x‖ := by
       congr with x
       simp only [norm_mul, Complex.norm_eq_abs]
       rw_mod_cast [mul_assoc, mul_comm Complex.I, Complex.abs_exp_ofReal_mul_I]
       ring
-    _ ≤ ∫ (_ : ℝ) in (0 : ℝ)..(2 * Real.pi), C := by
+    _ ≤ ∫ (_ : ℝ) in (0 : ℝ)..(2 * π), C := by
       refine intervalIntegral.integral_mono_on Real.two_pi_pos.le ?_ intervalIntegrable_const
         fun x hx ↦ f_bounded x hx
       /-Could specify `aestronglyMeasurable` and `intervalIntegrable` intead of `f_continuous`. -/
       exact IntervalIntegrable.intervalIntegrable_norm_iff f_continuous.aestronglyMeasurable |>.mpr
         (f_continuous.intervalIntegrable _ _)
-    _ = C * (2 * Real.pi) := by simp; ring
+    _ = C * (2 * π) := by simp; ring
 
 /-TODO: Assumptions might be weakened. -/
 lemma periodic_deriv {𝕜 : Type} [NontriviallyNormedField 𝕜] {F : Type} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
@@ -116,13 +112,13 @@ lemma periodic_deriv {𝕜 : Type} [NontriviallyNormedField 𝕜] {F : Type} [No
 
 /-TODO: might be generalized. -/
 /-TODO: The assumption periodicf is probably not needed actually. -/
-lemma fourierCoeffOn_ContDiff_two_bound {f : ℝ → ℂ} (periodicf : f.Periodic (2 * Real.pi)) (fdiff : ContDiff ℝ 2 f) :
+lemma fourierCoeffOn_ContDiff_two_bound {f : ℝ → ℂ} (periodicf : f.Periodic (2 * π)) (fdiff : ContDiff ℝ 2 f) :
     ∃ C, ∀ n ≠ 0, Complex.abs (fourierCoeffOn Real.two_pi_pos f n) ≤ C / n ^ 2 := by
-  have h : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt f (deriv f x) x := by
+  have h : ∀ x ∈ Set.uIcc 0 (2 * π), HasDerivAt f (deriv f x) x := by
     intro x _
     rw [hasDerivAt_deriv_iff]
     exact fdiff.differentiable (by norm_num) _
-  have h' : ∀ x ∈ Set.uIcc 0 (2 * Real.pi), HasDerivAt (deriv f) (deriv (deriv f) x) x := by
+  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) _
@@ -130,12 +126,12 @@ lemma fourierCoeffOn_ContDiff_two_bound {f : ℝ → ℂ} (periodicf : f.Periodi
   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']
     · have h1 := periodicf 0
-      have periodic_deriv_f : (deriv f).Periodic (2 * Real.pi) := periodic_deriv (fdiff.of_le one_le_two) periodicf
+      have periodic_deriv_f : (deriv f).Periodic (2 * π) := periodic_deriv (fdiff.of_le one_le_two) periodicf
       have h2 := periodic_deriv_f 0
       simp at h1 h2
       simp [h1, h2]
       ring_nf
-      simp [mul_inv_cancel, one_mul, Real.pi_pos.ne.symm]
+      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
@@ -179,13 +175,13 @@ lemma int_sum_nat {β : Type*} [AddCommGroup β] [TopologicalSpace β] [Continuo
       linarith
 
 
-lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : f.Periodic (2 * Real.pi)) (fdiff : ContDiff ℝ 2 f) {ε : ℝ} (εpos : ε > 0) :
-    ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), ‖f x - S_ N f x‖ ≤ ε := by
-  have fact_two_pi_pos : Fact (0 < 2 * Real.pi) := by
+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]
     exact Real.two_pi_pos
-  set g : C(AddCircle (2 * Real.pi), ℂ) := ⟨AddCircle.liftIco (2*Real.pi) 0 f, AddCircle.liftIco_continuous ((periodicf 0).symm) fdiff.continuous.continuousOn⟩ with g_def
-  have two_pi_pos' : 0 < 0 + 2 * Real.pi := by linarith [Real.two_pi_pos]
+  set g : C(AddCircle (2 * π), ℂ) := ⟨AddCircle.liftIco (2*π) 0 f, AddCircle.liftIco_continuous ((periodicf 0).symm) fdiff.continuous.continuousOn⟩ with g_def
+  have two_pi_pos' : 0 < 0 + 2 * π := by linarith [Real.two_pi_pos]
   have fourierCoeff_correspondence {i : ℤ} : fourierCoeff g i = fourierCoeffOn two_pi_pos' f i := fourierCoeff_liftIco_eq f i
   simp at fourierCoeff_correspondence
   have function_sum : HasSum (fun (i : ℤ) => fourierCoeff g i • fourier i) g := by
@@ -216,13 +212,13 @@ lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : f.Periodi
   convert this.le using 2
   congr 1
   · rw [g_def, ContinuousMap.coe_mk]
-    by_cases h : x = 2 * Real.pi
-    · conv => lhs; rw [h, ← zero_add  (2 * Real.pi), periodicf]
-      have := AddCircle.coe_add_period (2 * Real.pi) 0
+    by_cases h : x = 2 * π
+    · conv => lhs; rw [h, ← zero_add  (2 * π), periodicf]
+      have := AddCircle.coe_add_period (2 * π) 0
       rw [zero_add] at this
       rw [h, this, AddCircle.liftIco_coe_apply]
-      simp [Real.pi_pos]
-    · have : x ∈ Set.Ico 0 (2 * Real.pi) := by
+      simp [pi_pos]
+    · have : x ∈ Set.Ico 0 (2 * π) := by
         use hx.1
         exact lt_of_le_of_ne hx.2 h
       simp [AddCircle.liftIco_coe_apply, zero_add, this]
diff --git a/Carleson/Classical/Basic.lean b/Carleson/Classical/Basic.lean
index 505145e6..597c3002 100644
--- a/Carleson/Classical/Basic.lean
+++ b/Carleson/Classical/Basic.lean
@@ -7,14 +7,13 @@ import Mathlib.Analysis.Convolution
 
 import Carleson.Classical.Helper
 
-open BigOperators
-open Finset
+open BigOperators Finset Real
 
 noncomputable section
 
 
 def partialFourierSum (N : ℕ) (f : ℝ → ℂ) (x : ℝ) : ℂ := ∑ n ∈ Icc (-(N : ℤ)) N,
-    fourierCoeffOn Real.two_pi_pos f n * fourier n (x : AddCircle (2 * Real.pi))
+    fourierCoeffOn Real.two_pi_pos f n * fourier n (x : AddCircle (2 * π))
 
 --TODO: Add an AddCircle version?
 /-
@@ -53,13 +52,13 @@ lemma fourierCoeffOn_sub {a b : ℝ} {hab : a < b} {f g : ℝ → ℂ} {n : ℤ}
   rw [sub_eq_add_neg, fourierCoeffOn_add hf hg.neg, fourierCoeffOn_neg, ← sub_eq_add_neg]
 
 @[simp]
-lemma partialFourierSum_add {f g : ℝ → ℂ} {N : ℕ} (hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) (hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)) :
+lemma partialFourierSum_add {f g : ℝ → ℂ} {N : ℕ} (hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * π)) (hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * π)) :
   S_ N (f + g) = S_ N f + S_ N g := by
   ext x
   simp [partialFourierSum, sum_add_distrib, fourierCoeffOn_add hf hg, add_mul]
 
 @[simp]
-lemma partialFourierSum_sub {f g : ℝ → ℂ} {N : ℕ} (hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)) (hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)) :
+lemma partialFourierSum_sub {f g : ℝ → ℂ} {N : ℕ} (hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * π)) (hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * π)) :
   S_ N (f - g) = S_ N f - S_ N g := by
   ext x
   simp [partialFourierSum, sum_sub_distrib, fourierCoeffOn_sub hf hg, sub_mul]
@@ -71,10 +70,10 @@ lemma partialFourierSum_mul {f: ℝ → ℂ} {a : ℂ} {N : ℕ}:
   simp [partialFourierSum, mul_sum, fourierCoeffOn_mul, mul_assoc]
 
 lemma fourier_periodic {n : ℤ} :
-    (fun (x : ℝ) ↦ fourier n (x : AddCircle (2 * Real.pi))).Periodic (2 * Real.pi) := by
+    (fun (x : ℝ) ↦ fourier n (x : AddCircle (2 * π))).Periodic (2 * π) := by
     simp
 
-lemma partialFourierSum_periodic {f : ℝ → ℂ} {N : ℕ} : (S_ N f).Periodic (2 * Real.pi) := by
+lemma partialFourierSum_periodic {f : ℝ → ℂ} {N : ℕ} : (S_ N f).Periodic (2 * π) := by
     simp [Function.Periodic, partialFourierSum, fourier_periodic]
 
 --TODO: maybe generalize to (hc : ContinuousOn f (Set.Icc 0 T)) and leave out condition (hT : 0 < T)
@@ -101,7 +100,7 @@ lemma Function.Periodic.uniformContinuous_of_continuous {f : ℝ → ℂ} {T : 
 
 
 lemma fourier_uniformContinuous {n : ℤ} :
-    UniformContinuous (fun (x : ℝ) ↦ fourier n (x : AddCircle (2 * Real.pi))) := by
+    UniformContinuous (fun (x : ℝ) ↦ fourier n (x : AddCircle (2 * π))) := by
   apply fourier_periodic.uniformContinuous_of_continuous Real.two_pi_pos (Continuous.continuousOn _)
   continuity
 
@@ -110,16 +109,16 @@ lemma partialFourierSum_uniformContinuous {f : ℝ → ℂ} {N : ℕ} : UniformC
     (Continuous.continuousOn (continuous_finset_sum _ _))
   continuity
 
-theorem strictConvexOn_cos_Icc : StrictConvexOn ℝ (Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2)) Real.cos := by
+theorem strictConvexOn_cos_Icc : StrictConvexOn ℝ (Set.Icc (π / 2) (π + π / 2)) Real.cos := by
   apply strictConvexOn_of_deriv2_pos (convex_Icc _ _) Real.continuousOn_cos fun x hx => ?_
   rw [interior_Icc] at hx
   simp [Real.cos_neg_of_pi_div_two_lt_of_lt hx.1 hx.2]
 
-lemma lower_secant_bound' {η : ℝ}  {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_le : |x| ≤ 2 * Real.pi - η) :
-    (2 / Real.pi) * η ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by
+lemma lower_secant_bound' {η : ℝ}  {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_le : |x| ≤ 2 * π - η) :
+    (2 / π) * η ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by
   by_cases ηpos : η ≤ 0
-  · calc (2 / Real.pi) * η
-    _ ≤ 0 := mul_nonpos_of_nonneg_of_nonpos (div_nonneg zero_le_two Real.pi_pos.le) ηpos
+  · calc (2 / π) * η
+    _ ≤ 0 := mul_nonpos_of_nonneg_of_nonpos (div_nonneg zero_le_two pi_pos.le) ηpos
     _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := norm_nonneg _
   push_neg at ηpos
   wlog x_nonneg : 0 ≤ x generalizing x
@@ -128,23 +127,23 @@ lemma lower_secant_bound' {η : ℝ}  {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_l
           ←Complex.exp_conj, map_mul, Complex.conj_I, neg_mul, Complex.conj_ofReal]
     · rwa [abs_neg]
   rw [abs_of_nonneg x_nonneg] at *
-  wlog x_le_pi : x ≤ Real.pi generalizing x
-  · convert (@this (2 * Real.pi - x) _ _ _ _) using 1
+  wlog x_le_pi : x ≤ π generalizing x
+  · convert (@this (2 * π - x) _ _ _ _) using 1
     · rw [Complex.norm_eq_abs, ← Complex.abs_conj]
       simp [← Complex.exp_conj, mul_sub, Complex.conj_ofReal, Complex.exp_sub,
-        mul_comm Complex.I (2 * Real.pi), Complex.exp_two_pi_mul_I, ←inv_eq_one_div, ←Complex.exp_neg]
+        mul_comm Complex.I (2 * π), Complex.exp_two_pi_mul_I, ←inv_eq_one_div, ←Complex.exp_neg]
     all_goals linarith
-  by_cases h : x ≤ Real.pi / 2
-  · calc (2 / Real.pi) * η
-    _ ≤ (2 / Real.pi) * x := by gcongr
-    _ = (1 - (2 / Real.pi) * x) * Real.sin 0 + ((2 / Real.pi) * x) * Real.sin (Real.pi / 2) := by simp
-    _ ≤ Real.sin ((1 - (2 / Real.pi) * x) * 0 + ((2 / Real.pi) * x) * (Real.pi / 2)) := by
-      apply (strictConcaveOn_sin_Icc.concaveOn).2 (by simp [Real.pi_nonneg])
+  by_cases h : x ≤ π / 2
+  · calc (2 / π) * η
+    _ ≤ (2 / π) * x := by gcongr
+    _ = (1 - (2 / π) * x) * Real.sin 0 + ((2 / π) * x) * Real.sin (π / 2) := by simp
+    _ ≤ Real.sin ((1 - (2 / π) * x) * 0 + ((2 / π) * x) * (π / 2)) := by
+      apply (strictConcaveOn_sin_Icc.concaveOn).2 (by simp [pi_nonneg])
       · simp
-        constructor <;> linarith [Real.pi_nonneg]
+        constructor <;> linarith [pi_nonneg]
       · rw [sub_nonneg, mul_comm]
-        exact mul_le_of_nonneg_of_le_div (by norm_num) (div_nonneg (by norm_num) Real.pi_nonneg) (by simpa)
-      · exact mul_nonneg (div_nonneg (by norm_num) Real.pi_nonneg) x_nonneg
+        exact mul_le_of_nonneg_of_le_div (by norm_num) (div_nonneg (by norm_num) pi_nonneg) (by simpa)
+      · exact mul_nonneg (div_nonneg (by norm_num) pi_nonneg) x_nonneg
       · simp
     _ = Real.sin x := by field_simp
     _ ≤ Real.sqrt ((Real.sin x) ^ 2) := by
@@ -160,19 +159,19 @@ lemma lower_secant_bound' {η : ℝ}  {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_l
         · simp [pow_two_nonneg]
         · linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
   · push_neg at h
-    calc (2 / Real.pi) * η
-    _ ≤ (2 / Real.pi) * x := by gcongr
-    _ = 1 - ((1 - (2 / Real.pi) * (x - Real.pi / 2)) * Real.cos (Real.pi / 2) + ((2 / Real.pi) * (x - Real.pi / 2)) * Real.cos (Real.pi)) := by
+    calc (2 / π) * η
+    _ ≤ (2 / π) * x := by gcongr
+    _ = 1 - ((1 - (2 / π) * (x - π / 2)) * Real.cos (π / 2) + ((2 / π) * (x - π / 2)) * Real.cos (π)) := by
       field_simp
       ring
-    _ ≤ 1 - (Real.cos ((1 - (2 / Real.pi) * (x - Real.pi / 2)) * (Real.pi / 2) + (((2 / Real.pi) * (x - Real.pi / 2)) * (Real.pi)))) := by
+    _ ≤ 1 - (Real.cos ((1 - (2 / π) * (x - π / 2)) * (π / 2) + (((2 / π) * (x - π / 2)) * (π)))) := by
       gcongr
-      apply (strictConvexOn_cos_Icc.convexOn).2 (by simp [Real.pi_nonneg])
+      apply (strictConvexOn_cos_Icc.convexOn).2 (by simp [pi_nonneg])
       · simp
-        constructor <;> linarith [Real.pi_nonneg]
+        constructor <;> linarith [pi_nonneg]
       · rw [sub_nonneg, mul_comm]
-        exact mul_le_of_nonneg_of_le_div (by norm_num) (div_nonneg (by norm_num) Real.pi_nonneg) (by simpa)
-      · exact mul_nonneg (div_nonneg (by norm_num) Real.pi_nonneg) (by linarith [h])
+        exact mul_le_of_nonneg_of_le_div (by norm_num) (div_nonneg (by norm_num) pi_nonneg) (by simpa)
+      · exact mul_nonneg (div_nonneg (by norm_num) pi_nonneg) (by linarith [h])
       · simp
     _ = 1 - Real.cos x := by congr; field_simp; ring
     _ ≤ Real.sqrt ((1 - Real.cos x) ^ 2) := by
@@ -189,7 +188,7 @@ lemma lower_secant_bound' {η : ℝ}  {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_l
         · linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
 
 /-Slightly weaker version of Lemma 11..1.9 (lower secant bound) with simplified constant. -/
-lemma lower_secant_bound {η : ℝ} {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)) (xAbs : η ≤ |x|) :
+lemma lower_secant_bound {η : ℝ} {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * π + η) (2 * π - η)) (xAbs : η ≤ |x|) :
     η / 2 ≤ Complex.abs (1 - Complex.exp (Complex.I * x)) := by
   by_cases ηpos : η < 0
   · calc η / 2
@@ -197,13 +196,13 @@ lemma lower_secant_bound {η : ℝ} {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * Real.p
     _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := norm_nonneg _
   push_neg at ηpos
   calc η / 2
-  _ ≤ (2 / Real.pi) * η := by
+  _ ≤ (2 / π) * η := by
     ring_nf
     rw [mul_assoc]
     gcongr
     field_simp
-    rw [div_le_div_iff (by norm_num) Real.pi_pos]
-    linarith [Real.pi_le_four]
+    rw [div_le_div_iff (by norm_num) pi_pos]
+    linarith [pi_le_four]
   _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by
     apply lower_secant_bound' xAbs
     rw [abs_le, neg_sub', sub_neg_eq_add, neg_mul_eq_neg_mul]
diff --git a/Carleson/Classical/CarlesonOnTheRealLine.lean b/Carleson/Classical/CarlesonOnTheRealLine.lean
index 03b429c4..d777f7cd 100644
--- a/Carleson/Classical/CarlesonOnTheRealLine.lean
+++ b/Carleson/Classical/CarlesonOnTheRealLine.lean
@@ -4,17 +4,12 @@
 -/
 
 import Carleson.TwoSidedMetricCarleson
-import Carleson.Classical.Basic
-import Carleson.Classical.Helper
-import Carleson.Classical.HilbertKernel
 import Carleson.Classical.CarlesonOperatorReal
 import Carleson.Classical.VanDerCorput
 
-import Mathlib.Analysis.Fourier.AddCircle
-
 noncomputable section
 
-open MeasureTheory Function Metric Bornology
+open MeasureTheory Function Metric Bornology Real
 
 --#lint
 
@@ -445,7 +440,7 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
         push_cast
         rw [_root_.sub_mul]
         norm_cast
-      _ ≤ 2 * Real.pi * ((x + r) - (x - r)) * (B + L * ((x + r) - (x - r)) / 2) * (1 + |((↑f - ↑g) : ℤ)| * ((x + r) - (x - r)))⁻¹ := by
+      _ ≤ 2 * π * ((x + r) - (x - r)) * (B + L * ((x + r) - (x - r)) / 2) * (1 + |((↑f - ↑g) : ℤ)| * ((x + r) - (x - r)))⁻¹ := by
         apply van_der_Corput (by linarith)
         · rw [lipschitzWith_iff_dist_le_mul]
           intro x y
@@ -495,13 +490,13 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
           use y
           rw [Real.ball_eq_Ioo]
           use hy
-      _ = 2 * Real.pi * (2 * r) * (B + r * L) * (1 + 2 * r * |((↑f - ↑g) : ℤ)|)⁻¹ := by
+      _ = 2 * π * (2 * r) * (B + r * L) * (1 + 2 * r * |((↑f - ↑g) : ℤ)|)⁻¹ := by
         ring
       _ ≤ (2 ^ 4 : ℕ) * (2 * r) * iLipNorm ϕ x r * (1 + 2 * r * ↑|(↑f - ↑g : ℤ)|) ^ (- (1 / (4 : ℝ))) := by
         gcongr
         · exact mul_nonneg (mul_nonneg (by norm_num) (by linarith)) (iLipNorm_nonneg r_pos.le)
         · norm_num
-          linarith [Real.pi_le_four]
+          linarith [pi_le_four]
         · unfold iLipNorm
           gcongr
           apply le_of_eq Bdef
diff --git a/Carleson/Classical/ClassicalCarleson.lean b/Carleson/Classical/ClassicalCarleson.lean
index 1f7c3b35..13dec313 100644
--- a/Carleson/Classical/ClassicalCarleson.lean
+++ b/Carleson/Classical/ClassicalCarleson.lean
@@ -1,13 +1,11 @@
 /- This file contains the proof of the classical Carleson theorem from Section 11.1. -/
 
-import Carleson.MetricCarleson
-import Carleson.Classical.Basic
 import Carleson.Classical.Approximation
 import Carleson.Classical.ControlApproximationEffect
 
 import Mathlib.Analysis.Fourier.AddCircle
 
-open MeasureTheory
+open MeasureTheory Real
 
 noncomputable section
 
@@ -15,10 +13,10 @@ local notation "S_" => partialFourierSum
 
 /- Theorem 1.1 (Classical Carleson) -/
 theorem classical_carleson {f : ℝ → ℂ}
-    (cont_f : Continuous f) (periodic_f : f.Periodic (2 * Real.pi))
+    (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π))
     {ε : ℝ} (εpos : 0 < ε) :
-    ∃ E ⊆ Set.Icc 0 (2 * Real.pi), MeasurableSet E ∧ volume.real E ≤ ε ∧
-    ∃ N₀, ∀ x ∈ (Set.Icc 0 (2 * Real.pi)) \ E, ∀ N > N₀,
+    ∃ E ⊆ Set.Icc 0 (2 * π), MeasurableSet E ∧ volume.real E ≤ ε ∧
+    ∃ N₀, ∀ x ∈ (Set.Icc 0 (2 * π)) \ E, ∀ N > N₀,
     ‖f x - S_ N f x‖ ≤ ε := by
   set ε' := ε / 4 / C_control_approximation_effect ε with ε'def
   have ε'pos : ε' > 0 := div_pos (div_pos εpos (by norm_num)) (C_control_approximation_effect_pos εpos)
@@ -31,7 +29,7 @@ theorem classical_carleson {f : ℝ → ℂ}
 
   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 * Real.pi) := periodic_f₀.sub periodic_f
+  have h_periodic : h.Periodic (2 * π) := periodic_f₀.sub periodic_f
   have h_bound : ∀ x, ‖h x‖ ≤ ε' := by
     intro x
     simp [hdef]
@@ -56,7 +54,7 @@ theorem classical_carleson {f : ℝ → ℂ}
     · exact hf₀ x
     · exact hN₀ N NgtN₀ x hx.1
     · have := hE x hx N
-      rw [hdef, partialFourierSum_sub (contDiff_f₀.continuous.intervalIntegrable 0 (2 * Real.pi)) (cont_f.intervalIntegrable 0 (2 * Real.pi))] at this
+      rw [hdef, partialFourierSum_sub (contDiff_f₀.continuous.intervalIntegrable 0 (2 * π)) (cont_f.intervalIntegrable 0 (2 * π))] at this
       apply le_trans this
       rw [ε'def, mul_div_cancel₀ _ (C_control_approximation_effect_pos εpos).ne.symm]
   _ ≤ (ε / 2) + (ε / 4) + (ε / 4) := by
@@ -69,8 +67,8 @@ theorem classical_carleson {f : ℝ → ℂ}
 
 
 
-theorem carleson_interval {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * Real.pi)) :
-    ∀ᵐ x ∂volume.restrict (Set.Icc 0 (2 * Real.pi)),
+theorem carleson_interval {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π)) :
+    ∀ᵐ x ∂volume.restrict (Set.Icc 0 (2 * π)),
       Filter.Tendsto (S_ · f x) Filter.atTop (nhds (f x)) := by
 
   let δ (k : ℕ) : ℝ := 1 / (k + 1) --arbitrary sequence tending to zero
@@ -127,7 +125,7 @@ theorem carleson_interval {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f
   let E := ⋂ (k : ℕ), Eδ k
 
   -- Show that it has the desired property.
-  have hE : ∀ x ∈ (Set.Icc 0 (2 * Real.pi)) \ E, Filter.Tendsto (S_ · f x) Filter.atTop (nhds (f x)) := by
+  have hE : ∀ x ∈ (Set.Icc 0 (2 * π)) \ E, Filter.Tendsto (S_ · f x) Filter.atTop (nhds (f x)) := by
     intro x hx
     rw [Set.diff_iInter, Set.mem_iUnion] at hx
     rcases hx with ⟨k,hk⟩
@@ -206,7 +204,7 @@ lemma Function.Periodic.ae_of_ae_restrict {T : ℝ} (hT : 0 < T) {a : ℝ} {P :
 end section
 
 /- Carleson's theorem asserting a.e. convergence of the partial Fourier sums for continous functions. -/
-theorem carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * Real.pi)) :
+theorem carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π)) :
     ∀ᵐ x, Filter.Tendsto (S_ · f x) Filter.atTop (nhds (f x)) := by
   -- Reduce to a.e. convergence on [0,2π]
   apply @Function.Periodic.ae_of_ae_restrict _ Real.two_pi_pos 0
diff --git a/Carleson/Classical/ControlApproximationEffect.lean b/Carleson/Classical/ControlApproximationEffect.lean
index 7fbf077e..534ce469 100644
--- a/Carleson/Classical/ControlApproximationEffect.lean
+++ b/Carleson/Classical/ControlApproximationEffect.lean
@@ -1,23 +1,17 @@
 /- This file contains most of Section 11.6 (The error bound) from the blueprint.
    The main result is control_approximation_effect.
 -/
-import Carleson.MetricCarleson
-import Carleson.Classical.Helper
-import Carleson.Classical.Basic
-import Carleson.Classical.HilbertKernel
-import Carleson.Classical.DirichletKernel
-import Carleson.Classical.CarlesonOperatorReal
 import Carleson.Classical.CarlesonOnTheRealLine
-
-import Mathlib.Analysis.Fourier.AddCircle
-
+import Carleson.Classical.DirichletKernel
 
 noncomputable section
 
 local notation "T" => carlesonOperatorReal K
 local notation "S_" => partialFourierSum
 
+open scoped Real
 open MeasureTheory
+open Real (pi_pos)
 
 
 /- TODO: might be generalized. -/
@@ -90,13 +84,13 @@ lemma Dirichlet_Hilbert_eq {N : ℕ} {x : ℝ} :
   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 (-Real.pi) Real.pi):
-    ‖dirichletKernel' N (x) - (exp (I * (-N * x)) * k x + conj (exp (I * (-N * x)) * k x))‖ ≤ Real.pi := by
+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
   · rw [sub_eq_zero] at h
     rw [dirichletKernel'_eq_zero h.symm]
-    simp [Real.pi_pos.le]
+    simp [pi_pos.le]
   push_neg at h
   conv => pattern (dirichletKernel' N x); rw [← (one_mul (dirichletKernel' N x))]
   rw [← sub_mul]
@@ -126,15 +120,15 @@ lemma Dirichlet_Hilbert_diff {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc (-Real.pi)
         norm_cast
         rw [abs_exp_ofReal_mul_I]
     _ = 2 * (|x| / ‖1 - exp (I * x)‖) := by ring
-    _ ≤ 2 * (Real.pi / 2) := by
+    _ ≤ 2 * (π / 2) := by
       gcongr 2 * ?_
-      rw [div_le_iff₀' (by rwa [norm_pos_iff]), ← div_le_iff₀ (by linarith [Real.pi_pos]),
+      rw [div_le_iff₀' (by rwa [norm_pos_iff]), ← div_le_iff₀ (by linarith [pi_pos]),
         div_div_eq_mul_div, mul_div_assoc, mul_comm]
       apply lower_secant_bound' (by rfl)
-      have : |x| ≤ Real.pi := by
+      have : |x| ≤ π := by
         rwa [abs_le]
       linarith
-    _ = Real.pi := by ring
+    _ = π := by ring
 
 
 section
@@ -148,28 +142,28 @@ lemma le_iSup_of_tendsto {α β} [TopologicalSpace α] [CompleteLinearOrder α]
   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 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-Real.pi) (3 * Real.pi)) {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 <;>
   · rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le (by linarith)]
     apply hf.mono_set
-    rw [Set.uIcc_of_le (by linarith), Set.uIcc_of_le (by linarith [Real.pi_pos])]
+    rw [Set.uIcc_of_le (by linarith), Set.uIcc_of_le (by linarith [pi_pos])]
     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 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-Real.pi) (3 * Real.pi)) {N : ℕ} :
-    IntervalIntegrable (fun y ↦ f y * dirichletKernel' N (x - y)) volume (x - Real.pi) (x + Real.pi) := by
+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
   · use (2 * N + 1)
     intro y
     apply norm_dirichletKernel'_le
   · rw [Set.uIcc_of_le, Set.uIcc_of_le]
     apply Set.Icc_subset_Icc
-    all_goals linarith [hx.1, hx.2, Real.pi_pos]
+    all_goals linarith [hx.1, hx.2, pi_pos]
 
-lemma intervalIntegrable_mul_dirichletKernel'_max {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-Real.pi) (3 * Real.pi)) {N : ℕ} :
-    IntervalIntegrable (fun y ↦ f y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) volume (x - Real.pi) (x + Real.pi) := 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 _)
   use 1
@@ -178,33 +172,33 @@ lemma intervalIntegrable_mul_dirichletKernel'_max {x : ℝ} (hx : x ∈ Set.Icc
   rw [_root_.abs_of_nonneg (le_max_right _ _)]
   simp
 
-lemma intervalIntegrable_mul_dirichletKernel'_max' {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-Real.pi) (3 * Real.pi)) {N : ℕ} :
-    IntervalIntegrable (fun y ↦ f y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y))) volume (x - Real.pi) (x + Real.pi) := 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)
 
-lemma domain_reformulation {g : ℝ → ℂ} (hg : IntervalIntegrable g volume (-Real.pi) (3 * Real.pi)) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) :
-      ∫ (y : ℝ) in x - Real.pi..x + Real.pi,
+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 _
-    _ = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 Real.pi}, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) := by
+    _ = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 π}, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) := by
       rw [annulus_real_eq (le_refl 0), integral_union (by simp) measurableSet_Ioo, ← integral_Ioc_eq_integral_Ioo, ← integral_union (Set.disjoint_of_subset_right Set.Ioo_subset_Ioc_self (by simp)) measurableSet_Ioo,
-        intervalIntegral.integral_of_le (by linarith [Real.pi_pos]), integral_Ioc_eq_integral_Ioo,
-        sub_zero, add_zero, Set.Ioc_union_Ioo_eq_Ioo (by linarith [Real.pi_pos]) (by linarith [Real.pi_pos])]
+        intervalIntegral.integral_of_le (by linarith [pi_pos]), integral_Ioc_eq_integral_Ioo,
+        sub_zero, add_zero, Set.Ioc_union_Ioo_eq_Ioo (by linarith [pi_pos]) (by linarith [pi_pos])]
       --TODO: Many similar goals => improve this further?
-      · rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le (by linarith [Real.pi_pos])]
+      · rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le (by linarith [pi_pos])]
         apply (intervalIntegrable_mul_dirichletKernel'_max hx hg).mono_set
-        rw [Set.uIcc_of_le (by linarith [Real.pi_pos]), Set.uIcc_of_le (by linarith [Real.pi_pos])]
-        apply Set.Icc_subset_Icc_right (by linarith [Real.pi_pos])
+        rw [Set.uIcc_of_le (by linarith [pi_pos]), Set.uIcc_of_le (by linarith [pi_pos])]
+        apply Set.Icc_subset_Icc_right (by linarith [pi_pos])
       all_goals
-        rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le (by linarith [Real.pi_pos])]
+        rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le (by linarith [pi_pos])]
         apply (intervalIntegrable_mul_dirichletKernel'_max hx hg).mono_set
-        rw [Set.uIcc_of_le (by linarith [Real.pi_pos]), Set.uIcc_of_le (by linarith [Real.pi_pos])]
-      · apply Set.Icc_subset_Icc_left (by linarith [Real.pi_pos])
-      · apply Set.Icc_subset_Icc_right (by linarith [Real.pi_pos])
-      · apply Set.Icc_subset_Icc_left (by linarith [Real.pi_pos])
+        rw [Set.uIcc_of_le (by linarith [pi_pos]), Set.uIcc_of_le (by linarith [pi_pos])]
+      · apply Set.Icc_subset_Icc_left (by linarith [pi_pos])
+      · apply Set.Icc_subset_Icc_right (by linarith [pi_pos])
+      · apply Set.Icc_subset_Icc_left (by linarith [pi_pos])
     _ = ∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) := by
       rw [←integral_indicator annulus_measurableSet, ←integral_indicator annulus_measurableSet]
       congr with y
@@ -224,18 +218,18 @@ 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 * Real.pi)) {f : ℝ → ℂ} (hf : IntervalIntegrable f volume (-Real.pi) (3 * Real.pi)) {N : ℕ} :
+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 - Real.pi) (x + Real.pi) := intervalIntegrable_mul_dirichletKernel'_max hx hf
-  rw [intervalIntegrable_iff_integrableOn_Ioo_of_le (by linarith [Real.pi_pos])] at this
+  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
   rw [annulus_real_eq (by rfl)] at hy
   rcases hy with h | h <;> constructor <;> linarith [h.1, h.2, hx.1, hx.2, Real.two_le_pi]
 
 
-lemma le_CarlesonOperatorReal {g : ℝ → ℂ} (hg : IntervalIntegrable g volume (-Real.pi) (3 * Real.pi)) {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) :
-    ‖∫ (y : ℝ) in x - Real.pi..x + Real.pi, g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖₊
+lemma le_CarlesonOperatorReal {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))‖₊
     ≤ T g x + T (conj ∘ g) x := by
   rw [domain_reformulation hg hx]
   set s : ℕ → Set ℝ := fun n ↦ {y | dist x y ∈ Set.Ioo (1 / (n + 2 : ℝ)) 1} with sdef
@@ -387,47 +381,47 @@ lemma le_CarlesonOperatorReal {g : ℝ → ℂ} (hg : IntervalIntegrable g volum
         trivial
 
 lemma partialFourierSum_bound {δ : ℝ} (hδ : 0 < δ) {g : ℝ → ℂ} (measurable_g : Measurable g)
-    (periodic_g : Function.Periodic g (2 * Real.pi)) (bound_g : ∀ x, ‖g x‖ ≤ δ)
-    {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * Real.pi)) :
+    (periodic_g : Function.Periodic g (2 * π)) (bound_g : ∀ x, ‖g x‖ ≤ δ)
+    {N : ℕ} {x : ℝ} (hx : x ∈ Set.Icc 0 (2 * π)) :
     ‖S_ N g x‖₊
-      ≤ (T g x + T (conj ∘ g) x) / (ENNReal.ofReal (2 * Real.pi)) + ENNReal.ofReal (Real.pi * δ) := by
-  have intervalIntegrable_g : IntervalIntegrable g volume (-Real.pi) (3 * Real.pi) := intervalIntegrable_of_bdd measurable_g bound_g
+      ≤ (T g x + T (conj ∘ g) x) / (ENNReal.ofReal (2 * π)) + ENNReal.ofReal (π * δ) := by
+  have intervalIntegrable_g : IntervalIntegrable g volume (-π) (3 * π) := intervalIntegrable_of_bdd measurable_g bound_g
   have decomposition : S_ N g x
-      = (  (∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi),
+      = (  (∫ (y : ℝ) in (x - π)..(x + π),
               g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
-         + (∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi),
+         + (∫ (y : ℝ) in (x - π)..(x + π),
               g y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y))))
-        / (2 * Real.pi) := by
+        / (2 * π) := by
     calc S_ N g x
-      _ = (∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), g y * dirichletKernel' N (x - y)) / (2 * Real.pi) := by
+      _ = (∫ (y : ℝ) in (0 : ℝ)..(2 * π), g y * dirichletKernel' N (x - y)) / (2 * π) := by
         rw [partialFourierSum_eq_conv_dirichletKernel' (intervalIntegrable_g.mono_set _)]
         ring
         rw [Set.uIcc_of_le, Set.uIcc_of_le]
         apply Set.Icc_subset_Icc
-        all_goals linarith [Real.pi_pos]
-      _ = (∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), g y * dirichletKernel' N (x - y)) / (2 * Real.pi) := by
+        all_goals linarith [pi_pos]
+      _ = (∫ (y : ℝ) in (x - π)..(x + π), g y * dirichletKernel' N (x - y)) / (2 * π) := by
         --Shift domain of integration using periodicity
         congr 1
-        rw [← zero_add (2 * Real.pi), Function.Periodic.intervalIntegral_add_eq _ 0 (x - Real.pi)]
+        rw [← zero_add (2 * π), Function.Periodic.intervalIntegral_add_eq _ 0 (x - π)]
         congr 1
         ring
         exact (periodic_g.mul (dirichletKernel'_periodic.const_sub x))
-      _ = (  (∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
-           + (∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), g y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))) / (2 * Real.pi) := by
+      _ = (  (∫ (y : ℝ) in (x - π)..(x + π), g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
+           + (∫ (y : ℝ) in (x - π)..(x + π), g y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))) / (2 * π) := by
         --Split into two parts
         rw [← intervalIntegral.integral_add (intervalIntegrable_mul_dirichletKernel'_max hx intervalIntegrable_g) (intervalIntegrable_mul_dirichletKernel'_max' hx intervalIntegrable_g)]
         congr with y
         ring
 
   calc ENNReal.ofNNReal ‖S_ N g x‖₊
-    _ ≤ (  ‖∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖₊
-         + ‖∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), g y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖₊) / ENNReal.ofReal (2 * Real.pi) := by
-      rw [decomposition, nnnorm_div, ENNReal.coe_div (by simp [Real.pi_pos.ne.symm])]
+    _ ≤ (  ‖∫ (y : ℝ) in (x - π)..(x + π), g y * ((max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖₊
+         + ‖∫ (y : ℝ) in (x - π)..(x + π), g y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖₊) / ENNReal.ofReal (2 * π) := by
+      rw [decomposition, nnnorm_div, ENNReal.coe_div (by simp [pi_pos.ne.symm])]
       norm_cast
       gcongr
       · apply nnnorm_add_le
       · rw [← ofReal_norm_eq_coe_nnnorm, Real.norm_of_nonneg Real.two_pi_pos.le]
-    _ ≤ (T g x + T (⇑conj ∘ g) x + ENNReal.ofReal (Real.pi * δ * (2 * Real.pi))) / ENNReal.ofReal (2 * Real.pi) := by
+    _ ≤ (T g x + T (⇑conj ∘ g) x + ENNReal.ofReal (π * δ * (2 * π))) / ENNReal.ofReal (2 * π) := by
       gcongr
       · apply le_CarlesonOperatorReal intervalIntegrable_g hx
       · rw [ENNReal.ofReal]
@@ -435,22 +429,22 @@ lemma partialFourierSum_bound {δ : ℝ} (hδ : 0 < δ) {g : ℝ → ℂ} (measu
         apply NNReal.le_toNNReal_of_coe_le
         rw [coe_nnnorm]
 
-        calc ‖∫ (y : ℝ) in x - Real.pi..x + Real.pi, g y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖
-          _ ≤ (δ * Real.pi) * |(x + Real.pi) - (x - Real.pi)| := by
+        calc ‖∫ (y : ℝ) in x - π..x + π, g y * (dirichletKernel' N (x - y) - (max (1 - |x - y|) 0) * dirichletKernel' N (x - y))‖
+          _ ≤ (δ * π) * |(x + π) - (x - π)| := by
             apply intervalIntegral.norm_integral_le_of_norm_le_const
             intro y hy
-            rw [Set.uIoc_of_le (by linarith [Real.pi_pos])] at hy
+            rw [Set.uIoc_of_le (by linarith [pi_pos])] at hy
             rw [norm_mul]
             gcongr
             · apply bound_g
             · rw [Dirichlet_Hilbert_eq]
               apply Dirichlet_Hilbert_diff
               constructor <;> linarith [hy.1, hy.2]
-          _ = Real.pi * δ * (2 * Real.pi) := by
+          _ = π * δ * (2 * π) := by
             simp
             rw [←two_mul, _root_.abs_of_nonneg Real.two_pi_pos.le]
             ring
-    _ = (T g x + T (conj ∘ g) x) / ENNReal.ofReal (2 * Real.pi) + ENNReal.ofReal (Real.pi * δ) := by
+    _ = (T g x + T (conj ∘ g) x) / ENNReal.ofReal (2 * π) + ENNReal.ofReal (π * δ) := by
       rw [ENNReal.add_div]
       congr
       rw [← ENNReal.ofReal_div_of_pos Real.two_pi_pos, mul_div_assoc, div_self Real.two_pi_pos.ne.symm, mul_one]
@@ -485,10 +479,10 @@ lemma rcarleson_exceptional_set_estimate {δ : ℝ} (δpos : 0 < δ) {f : ℝ 
       ring
 
 lemma rcarleson_exceptional_set_estimate_specific {δ : ℝ} (δpos : 0 < δ) {f : ℝ → ℂ} (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ δ)
-    {E : Set ℝ} (measurableSetE : MeasurableSet E) (E_subset : E ⊆ Set.Icc 0 (2 * Real.pi)) {ε : ENNReal} (hE : ∀ x ∈ E, ε ≤ T f x) :
-      ε * volume E ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (2 * Real.pi + 2) ^ (2 : ℝ)⁻¹) * volume E ^ (2 : ℝ)⁻¹ := by
-  rw [ENNReal.ofReal_mul (by apply mul_nonneg δpos.le (C10_0_1_pos one_lt_two).le), ← ENNReal.ofReal_rpow_of_pos (by linarith [Real.pi_pos])]
-  set F := (Set.Ioo (0 - 1) (2 * Real.pi + 1))
+    {E : Set ℝ} (measurableSetE : MeasurableSet E) (E_subset : E ⊆ Set.Icc 0 (2 * π)) {ε : ENNReal} (hE : ∀ x ∈ E, ε ≤ T f x) :
+      ε * volume E ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (2 * π + 2) ^ (2 : ℝ)⁻¹) * volume E ^ (2 : ℝ)⁻¹ := by
+  rw [ENNReal.ofReal_mul (by apply mul_nonneg δpos.le (C10_0_1_pos one_lt_two).le), ← ENNReal.ofReal_rpow_of_pos (by linarith [pi_pos])]
+  set F := (Set.Ioo (0 - 1) (2 * π + 1))
   set h := F.indicator f with hdef
   have hh : ∀ x, ‖h x‖ ≤ δ * F.indicator 1 x := by
     intro x
@@ -504,43 +498,43 @@ lemma rcarleson_exceptional_set_estimate_specific {δ : ℝ} (δpos : 0 < δ) {f
     exact hE x hx
 
 
-def C_control_approximation_effect (ε : ℝ) := (C10_0_1 4 2 * (8 / (Real.pi * ε)) ^ (2 : ℝ)⁻¹) + Real.pi
+def C_control_approximation_effect (ε : ℝ) := (C10_0_1 4 2 * (8 / (π * ε)) ^ (2 : ℝ)⁻¹) + π
 
-lemma lt_C_control_approximation_effect {ε : ℝ} (εpos : 0 < ε) : Real.pi < C_control_approximation_effect ε := by
+lemma lt_C_control_approximation_effect {ε : ℝ} (εpos : 0 < ε) : π < C_control_approximation_effect ε := by
   rw [C_control_approximation_effect]
   apply lt_add_of_pos_of_le _ (by rfl)
   apply mul_pos (C10_0_1_pos (by norm_num))
   apply Real.rpow_pos_of_pos
   apply div_pos (by norm_num)
-  apply mul_pos Real.pi_pos εpos
+  apply mul_pos pi_pos εpos
 
-lemma C_control_approximation_effect_pos {ε : ℝ} (εpos : 0 < ε) : 0 < C_control_approximation_effect ε := lt_trans' (lt_C_control_approximation_effect εpos) Real.pi_pos
+lemma C_control_approximation_effect_pos {ε : ℝ} (εpos : 0 < ε) : 0 < C_control_approximation_effect ε := lt_trans' (lt_C_control_approximation_effect εpos) pi_pos
 
-lemma C_control_approximation_effect_eq {ε : ℝ} {δ : ℝ} (ε_nonneg : 0 ≤ ε) : C_control_approximation_effect ε * δ = ((δ * C10_0_1 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ * (2 / ε) ^ (2 : ℝ)⁻¹) / Real.pi) + Real.pi * δ := by
+lemma C_control_approximation_effect_eq {ε : ℝ} {δ : ℝ} (ε_nonneg : 0 ≤ ε) : C_control_approximation_effect ε * δ = ((δ * C10_0_1 4 2 * (4 * π) ^ (2 : ℝ)⁻¹ * (2 / ε) ^ (2 : ℝ)⁻¹) / π) + π * δ := by
   symm
   rw [C_control_approximation_effect, mul_comm, mul_div_right_comm, mul_comm δ, mul_assoc,
     mul_comm δ, ← mul_assoc, ← mul_assoc, ← add_mul, mul_comm _ (C10_0_1 4 2), mul_assoc]
   congr
   rw [Real.div_rpow, Real.div_rpow _ (mul_nonneg _ _), Real.mul_rpow, Real.mul_rpow]
   ring_nf
-  rw [mul_assoc, mul_comm (2 ^ _), mul_assoc, mul_assoc, mul_assoc, mul_comm (4 ^ _), ← mul_assoc Real.pi⁻¹,
-      ← Real.rpow_neg_one Real.pi, ← Real.rpow_add, mul_comm (Real.pi ^ _), ← mul_assoc (2 ^ _), ← Real.mul_rpow]
+  rw [mul_assoc, mul_comm (2 ^ _), mul_assoc, mul_assoc, mul_assoc, mul_comm (4 ^ _), ← mul_assoc π⁻¹,
+      ← Real.rpow_neg_one π, ← Real.rpow_add, mul_comm (π ^ _), ← mul_assoc (2 ^ _), ← Real.mul_rpow]
   congr
   norm_num
   ring_nf
   rw [neg_div, Real.rpow_neg]
-  all_goals linarith [Real.pi_pos]
+  all_goals linarith [pi_pos]
 
 
 
 /- 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 * Real.pi)) (h_bound : ∀ x, ‖h x‖ ≤ δ ) :
-    ∃ E ⊆ Set.Icc 0 (2 * Real.pi), MeasurableSet E ∧ volume.real E ≤ ε ∧ ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
+    {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
-  set E := {x ∈ Set.Icc 0 (2 * Real.pi) | ∃ N, ε' < abs (S_ N h x)} with Edef
-  have E_eq: E = Set.Icc 0 (2 * Real.pi) ∩ ⋃ N : ℕ, {x | ε' < ‖S_ N h x‖} := by
+  set E := {x ∈ Set.Icc 0 (2 * π) | ∃ N, ε' < abs (S_ N h x)} with Edef
+  have E_eq: E = Set.Icc 0 (2 * π) ∩ ⋃ N : ℕ, {x | ε' < ‖S_ N h x‖} := by
       rw [Edef]
       ext x
       simp
@@ -549,7 +543,7 @@ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ :
     apply measurableSet_Icc.inter (MeasurableSet.iUnion _)
     intro N
     apply measurableSet_lt measurable_const (Measurable.norm partialFourierSum_uniformContinuous.continuous.measurable)
-  have Esubset : E ⊆ Set.Icc 0 (2 * Real.pi) := by
+  have Esubset : E ⊆ Set.Icc 0 (2 * π) := by
     intro x hx
     rw [Edef] at hx
     simp at hx
@@ -567,64 +561,64 @@ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ :
     simp only [RCLike.star_def, Function.comp_apply, RingHomIsometric.is_iso]
     exact h_bound x
 
-  have le_operator_add : ∀ x ∈ E, ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) ≤ T h x + T (conj ∘ h) x := by
+  have le_operator_add : ∀ x ∈ E, ENNReal.ofReal ((ε' - π * δ) * (2 * π)) ≤ T h x + T (conj ∘ h) x := by
     intro x hx
     obtain ⟨xIcc, N, hN⟩ := hx
-    have : ENNReal.ofReal (Real.pi * δ * (2 * Real.pi)) ≠ ⊤ := ENNReal.ofReal_ne_top
+    have : ENNReal.ofReal (π * δ * (2 * π)) ≠ ⊤ := ENNReal.ofReal_ne_top
     rw [← (ENNReal.add_le_add_iff_right this)]
-    calc ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) + ENNReal.ofReal (Real.pi * δ * (2 * Real.pi))
-      _ = ENNReal.ofReal (2 * Real.pi) * ENNReal.ofReal ε' := by
+    calc ENNReal.ofReal ((ε' - π * δ) * (2 * π)) + ENNReal.ofReal (π * δ * (2 * π))
+      _ = ENNReal.ofReal (2 * π) * ENNReal.ofReal ε' := by
         rw [← ENNReal.ofReal_add, ← ENNReal.ofReal_mul Real.two_pi_pos.le]
         · ring_nf
         · apply mul_nonneg _ Real.two_pi_pos.le
           rw [ε'def, C_control_approximation_effect_eq εpos.le, add_sub_cancel_right]
-          apply div_nonneg (mul_nonneg _ (Real.rpow_nonneg (div_nonneg (by norm_num) εpos.le) _)) Real.pi_pos.le
+          apply div_nonneg (mul_nonneg _ (Real.rpow_nonneg (div_nonneg (by norm_num) εpos.le) _)) pi_pos.le
           rw [mul_assoc]
           apply mul_nonneg hδ.le (mul_nonneg (C10_0_1_pos one_lt_two).le (Real.rpow_nonneg _ _))
-          linarith [Real.pi_pos]
-        · apply mul_nonneg (mul_nonneg Real.pi_pos.le hδ.le) Real.two_pi_pos.le
-      _ ≤ ENNReal.ofReal (2 * Real.pi) * ‖S_ N h x‖₊ := by
+          linarith [pi_pos]
+        · apply mul_nonneg (mul_nonneg pi_pos.le hδ.le) Real.two_pi_pos.le
+      _ ≤ ENNReal.ofReal (2 * π) * ‖S_ N h x‖₊ := by
         rw [← ofReal_norm_eq_coe_nnnorm]
         gcongr
         exact hN.le
-      _ ≤ ENNReal.ofReal (2 * Real.pi) * ((T h x + T (conj ∘ h) x) / (ENNReal.ofReal (2 * Real.pi)) + ENNReal.ofReal (Real.pi * δ)) := by
+      _ ≤ ENNReal.ofReal (2 * π) * ((T h x + T (conj ∘ h) x) / (ENNReal.ofReal (2 * π)) + ENNReal.ofReal (π * δ)) := by
         gcongr
         apply partialFourierSum_bound hδ h_measurable h_periodic h_bound xIcc
-      _ = (T h x + T (conj ∘ h) x) + ENNReal.ofReal (Real.pi * δ * (2 * Real.pi)) := by
+      _ = (T h x + T (conj ∘ h) x) + ENNReal.ofReal (π * δ * (2 * π)) := by
         rw [mul_add]
         congr
-        · rw [ENNReal.mul_div_cancel' (by simp [Real.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
   have Evolume : volume E < ⊤ := by
     calc volume E
-      _ ≤ volume (Set.Icc 0 (2 * Real.pi)) := by
+      _ ≤ volume (Set.Icc 0 (2 * π)) := by
         apply measure_mono
         rw [E_eq]
         apply Set.inter_subset_left
-      _ = ENNReal.ofReal (2 * Real.pi) := by
+      _ = ENNReal.ofReal (2 * π) := by
         rw [Real.volume_Icc, sub_zero]
       _ < ⊤ := ENNReal.ofReal_lt_top
   obtain ⟨E', E'subset, measurableSetE', E'measure, h⟩ := ENNReal.le_on_subset volume measurableSetE (carlesonOperatorReal_measurable h_measurable h_bound) (carlesonOperatorReal_measurable (continuous_star.measurable.comp h_measurable) conj_h_bound) le_operator_add
   have E'volume : volume E' < ⊤ := lt_of_le_of_lt (measure_mono E'subset) Evolume
-  have E'volume_bound: ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * volume E' ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹) * (volume E') ^ (2 : ℝ)⁻¹ := by
-    calc ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * volume E'
-    _ = ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 * volume E' := by
+  have E'volume_bound: ENNReal.ofReal (π * (ε' - π * δ)) * volume E' ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (4 * π) ^ (2 : ℝ)⁻¹) * (volume E') ^ (2 : ℝ)⁻¹ := by
+    calc ENNReal.ofReal (π * (ε' - π * δ)) * volume E'
+    _ = ENNReal.ofReal ((ε' - π * δ) * (2 * π)) / 2 * volume E' := by
       rw [← ENNReal.ofReal_ofNat, ← ENNReal.ofReal_div_of_pos (by norm_num)]
       ring_nf
-    _ ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (2 * Real.pi + 2) ^ (2 : ℝ)⁻¹) * (volume E') ^ (2 : ℝ)⁻¹ := by
+    _ ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (2 * π + 2) ^ (2 : ℝ)⁻¹) * (volume E') ^ (2 : ℝ)⁻¹ := by
       rcases h with hE' | hE'
       · exact rcarleson_exceptional_set_estimate_specific hδ h_measurable h_bound measurableSetE' (E'subset.trans Esubset) hE'
       · refine rcarleson_exceptional_set_estimate_specific hδ ?_ conj_h_bound measurableSetE' (E'subset.trans Esubset) hE'
         exact ContinuousStar.continuous_star.measurable.comp h_measurable
-    _ ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹) * (volume E') ^ (2 : ℝ)⁻¹ := by
+    _ ≤ ENNReal.ofReal (δ * C10_0_1 4 2 * (4 * π) ^ (2 : ℝ)⁻¹) * (volume E') ^ (2 : ℝ)⁻¹ := by
       gcongr
       · exact mul_nonneg hδ.le (C10_0_1_pos one_lt_two).le
       · linarith [Real.two_le_pi]
-  have δ_mul_const_pos : 0 < δ * C10_0_1 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ := mul_pos (mul_pos hδ (C10_0_1_pos one_lt_two)) (Real.rpow_pos_of_pos (by linarith [Real.two_pi_pos]) _)
-  have ε'_δ_expression_pos : 0 < Real.pi * (ε' - Real.pi * δ) := by
-    rw [ε'def, C_control_approximation_effect_eq εpos.le, add_sub_cancel_right, mul_div_cancel₀ _ Real.pi_pos.ne.symm]
+  have δ_mul_const_pos : 0 < δ * C10_0_1 4 2 * (4 * π) ^ (2 : ℝ)⁻¹ := mul_pos (mul_pos hδ (C10_0_1_pos one_lt_two)) (Real.rpow_pos_of_pos (by linarith [Real.two_pi_pos]) _)
+  have ε'_δ_expression_pos : 0 < π * (ε' - π * δ) := by
+    rw [ε'def, C_control_approximation_effect_eq εpos.le, add_sub_cancel_right, mul_div_cancel₀ _ pi_pos.ne.symm]
     exact mul_pos δ_mul_const_pos (Real.rpow_pos_of_pos (div_pos (by norm_num) εpos) _)
   calc volume.real E
     _ ≤ 2 * volume.real E' := by
@@ -635,7 +629,7 @@ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ :
     _ = 2 * volume.real E' ^ ((1 + -(2 : ℝ)⁻¹) * 2) := by
       conv => lhs; rw [←Real.rpow_one (volume.real E')]
       norm_num
-    _ ≤ 2 * (δ * C10_0_1 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ / (Real.pi * (ε' - Real.pi * δ))) ^ (2 : ℝ) := by
+    _ ≤ 2 * (δ * C10_0_1 4 2 * (4 * π) ^ (2 : ℝ)⁻¹ / (π * (ε' - π * δ))) ^ (2 : ℝ) := by
       rw [Real.rpow_mul measureReal_nonneg]
       gcongr
       rw [Real.rpow_add' measureReal_nonneg (by norm_num), Real.rpow_one, le_div_iff₀' ε'_δ_expression_pos, ← mul_assoc]
@@ -649,7 +643,7 @@ lemma control_approximation_effect {ε : ℝ} (εpos : 0 < ε) {δ : ℝ} (hδ :
       apply Real.rpow_nonneg measureReal_nonneg
     _ = ε := by
       --We have chosen ε' such that this works.
-      rw [ε'def, C_control_approximation_effect_eq εpos.le, add_sub_cancel_right, mul_div_cancel₀ _ Real.pi_pos.ne.symm,
+      rw [ε'def, C_control_approximation_effect_eq εpos.le, add_sub_cancel_right, mul_div_cancel₀ _ pi_pos.ne.symm,
           div_mul_eq_div_div, div_self δ_mul_const_pos.ne.symm, one_div, Real.inv_rpow (Real.rpow_nonneg (div_nonneg zero_le_two εpos.le) _),
           ← Real.rpow_mul (div_nonneg zero_le_two εpos.le), inv_mul_cancel₀ (by norm_num), Real.rpow_one, inv_div]
       ring
diff --git a/Carleson/Classical/DirichletKernel.lean b/Carleson/Classical/DirichletKernel.lean
index f5509df3..91f68de1 100644
--- a/Carleson/Classical/DirichletKernel.lean
+++ b/Carleson/Classical/DirichletKernel.lean
@@ -6,23 +6,24 @@ import Mathlib.Analysis.Fourier.AddCircle
 import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
 import Mathlib.Analysis.Convolution
 
+open scoped Real
 open BigOperators Finset Complex MeasureTheory
 
 noncomputable section
 
 def dirichletKernel (N : ℕ) : ℝ → ℂ :=
-  fun x ↦ ∑ n in Icc (-Int.ofNat N) N, fourier n (x : AddCircle (2 * Real.pi))
+  fun x ↦ ∑ n in Icc (-Int.ofNat N) N, fourier n (x : AddCircle (2 * π))
 
 def dirichletKernel' (N : ℕ) : ℝ → ℂ :=
   fun x ↦ (exp (I * N * x) / (1 - exp (-I * x)) + exp (-I * N * x) / (1 - exp (I * x)))
 
-lemma dirichletKernel_periodic {N : ℕ} : Function.Periodic (dirichletKernel N) (2 * Real.pi) := by
+lemma dirichletKernel_periodic {N : ℕ} : Function.Periodic (dirichletKernel N) (2 * π) := by
   intro x
   simp_rw [dirichletKernel]
   congr
   simp
 
-lemma dirichletKernel'_periodic {N : ℕ} : Function.Periodic (dirichletKernel' N) (2 * Real.pi) := by
+lemma dirichletKernel'_periodic {N : ℕ} : Function.Periodic (dirichletKernel' N) (2 * π) := by
   intro x
   simp_rw [dirichletKernel']
   push_cast
@@ -127,7 +128,7 @@ lemma dirichletKernel'_eq_zero {N : ℕ} {x : ℝ} (h : cexp (I * x) = 1) : diri
 
 /- "a.e." version of previous lemma. -/
 lemma dirichletKernel_eq_ae {N : ℕ} : ∀ᵐ (x : ℝ), dirichletKernel N x = dirichletKernel' N x := by
-  have : {x | ¬dirichletKernel N x = dirichletKernel' N x} ⊆ {x | ∃ n : ℤ, n * (2 * Real.pi) = x} := by
+  have : {x | ¬dirichletKernel N x = dirichletKernel' N x} ⊆ {x | ∃ n : ℤ, n * (2 * π) = x} := by
     intro x hx
     simp at *
     by_contra h
@@ -143,7 +144,7 @@ lemma dirichletKernel_eq_ae {N : ℕ} : ∀ᵐ (x : ℝ), dirichletKernel N x =
   rw [ae_iff]
   apply measure_mono_null this
   apply Set.Countable.measure_zero
-  let f : ℤ → ℝ := fun n ↦ n * (2 * Real.pi)
+  let f : ℤ → ℝ := fun n ↦ n * (2 * π)
   apply Set.countable_range f
 
 lemma norm_dirichletKernel_le {N : ℕ} {x : ℝ} : ‖dirichletKernel N x‖ ≤ 2 * N + 1 := by
@@ -152,7 +153,7 @@ lemma norm_dirichletKernel_le {N : ℕ} {x : ℝ} : ‖dirichletKernel N x‖ 
     _ ≤ ∑ n ∈ Icc (-(N : ℤ)) N, ‖(fourier n) ↑x‖ := norm_sum_le _ _
     _ ≤ ∑ n ∈ Icc (-(N : ℤ)) N, 1 := by
       apply sum_le_sum
-      have : Fact (0 < 2 * Real.pi) := by rw [fact_iff]; exact Real.two_pi_pos
+      have : Fact (0 < 2 * π) := by rw [fact_iff]; exact Real.two_pi_pos
       exact fun n _ ↦ le_trans (ContinuousMap.norm_coe_le_norm (fourier n) x) (fourier_norm n).le
     _ = 2 * N + 1 := by
       rw_mod_cast [sum_const, Int.card_Icc, sub_neg_eq_add, nsmul_eq_mul, mul_one,
@@ -168,30 +169,30 @@ lemma norm_dirichletKernel'_le {N : ℕ} {x : ℝ} : ‖dirichletKernel' N x‖
     linarith
 
 /-First part of lemma 11.1.8 (Dirichlet kernel) from the blueprint.-/
-lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {N : ℕ} {x : ℝ} (h : IntervalIntegrable f volume 0 (2 * Real.pi)) :
-    partialFourierSum N f x = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel N (x - y)  := by
+lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {N : ℕ} {x : ℝ} (h : IntervalIntegrable f volume 0 (2 * π)) :
+    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]
-    _ = ∑ n in Icc (-(N : ℤ)) N, (1 / (2 * Real.pi - 0)) • ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by
+    _ = ∑ n in Icc (-(N : ℤ)) N, (1 / (2 * π - 0)) • ((∫ (y : ℝ) in (0 : ℝ)..2 * π, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by
       congr 1 with n
       rw [fourierCoeffOn_eq_integral, smul_mul_assoc]
-    _ = (1 / (2 * Real.pi)) * ∑ n in Icc (-(N : ℤ)) N, ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by
+    _ = (1 / (2 * π)) * ∑ n in Icc (-(N : ℤ)) N, ((∫ (y : ℝ) in (0 : ℝ)..2 * π, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by
       rw_mod_cast [← smul_sum, real_smul, sub_zero]
-    _ = (1 / (2 * Real.pi)) * ∑ n in Icc (-(N : ℤ)) N, ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y) * (fourier n) ↑x)) := by
+    _ = (1 / (2 * π)) * ∑ n in Icc (-(N : ℤ)) N, ((∫ (y : ℝ) in (0 : ℝ)..2 * π, (fourier (-n) ↑y • f y) * (fourier n) ↑x)) := by
       congr with n
       exact (intervalIntegral.integral_mul_const _ _).symm
-    _ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), ∑ n in Icc (-(N : ℤ)) N, (fourier (-n)) y • f y * (fourier n) x := by
+    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), ∑ n in Icc (-(N : ℤ)) N, (fourier (-n)) y • f y * (fourier n) x := by
       rw [← intervalIntegral.integral_finset_sum]
       exact fun _ _ ↦ IntervalIntegrable.mul_const
         (h.continuousOn_mul fourier_uniformContinuous.continuous.continuousOn) _
-    _ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * ∑ n in Icc (-(N : ℤ)) N, (fourier (-n)) y * (fourier n) x := by
+    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), f y * ∑ n in Icc (-(N : ℤ)) N, (fourier (-n)) y * (fourier n) x := by
       congr with y
       rw [mul_sum]
       congr with n
       rw [smul_eq_mul]
       ring
-    _ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel N (x - y) := by
+    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), f y * dirichletKernel N (x - y) := by
       congr with y
       rw [dirichletKernel]
       congr with n
@@ -200,15 +201,15 @@ lemma partialFourierSum_eq_conv_dirichletKernel {f : ℝ → ℂ} {N : ℕ} {x :
       field_simp
       rw [mul_sub, sub_eq_neg_add]
 
-lemma partialFourierSum_eq_conv_dirichletKernel' {f : ℝ → ℂ} {N : ℕ} {x : ℝ} (h : IntervalIntegrable f volume 0 (2 * Real.pi)) :
-    partialFourierSum N f x = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel' N (x - y)  := by
+lemma partialFourierSum_eq_conv_dirichletKernel' {f : ℝ → ℂ} {N : ℕ} {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 * Real.pi)) * ∫ (y : ℝ) in (x - 2 * Real.pi)..(x - 0), f (x - y) * dirichletKernel N y := by
+    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (x - 2 * π)..(x - 0), f (x - y) * dirichletKernel N y := by
       congr 1
       rw [← intervalIntegral.integral_comp_sub_left]
       simp
-    _ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (x - 2 * Real.pi)..(x - 0), f (x - y) * dirichletKernel' N y := by
+    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (x - 2 * π)..(x - 0), f (x - y) * dirichletKernel' N y := by
       congr 1
       apply intervalIntegral.integral_congr_ae (ae_imp_of_ae_restrict
         (ae_restrict_of_ae _))
@@ -220,7 +221,7 @@ lemma partialFourierSum_eq_conv_dirichletKernel' {f : ℝ → ℂ} {N : ℕ} {x
         exfalso
         exact h ha
       apply measure_mono_null this dirichletKernel_eq_ae
-    _ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel' N (x - y) := by
+    _ = (1 / (2 * π)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * π), f y * dirichletKernel' N (x - y) := by
       congr 1
       rw [← intervalIntegral.integral_comp_sub_left]
       simp
diff --git a/Carleson/Classical/HilbertKernel.lean b/Carleson/Classical/HilbertKernel.lean
index 80b83c08..a07ff63a 100644
--- a/Carleson/Classical/HilbertKernel.lean
+++ b/Carleson/Classical/HilbertKernel.lean
@@ -8,6 +8,7 @@ import Mathlib.Tactic.FunProp
 
 noncomputable section
 
+open scoped Real
 open Complex ComplexConjugate MeasureTheory
 
 def k (x : ℝ) : ℂ := max (1 - |x|) 0 / (1 - exp (I * x))
@@ -59,16 +60,16 @@ lemma Hilbert_kernel_bound {x y : ℝ} : ‖K x y‖ ≤ 2 ^ (2 : ℝ) / (2 * |x
           · simp
             calc |x - y|
               _ ≤ 1 := h.2.le
-              _ ≤ 2 * Real.pi - 1 := by rw [le_sub_iff_add_le]; linarith [Real.two_le_pi]
-              _ ≤ 2 * Real.pi + (x - y) := by
+              _ ≤ 2 * π - 1 := by rw [le_sub_iff_add_le]; linarith [Real.two_le_pi]
+              _ ≤ 2 * π + (x - y) := by
                 rw [sub_eq_add_neg]
                 gcongr
                 exact (abs_le.mp h.2.le).1
           · calc x - y
               _ ≤ |x - y| := le_abs_self (x - y)
               _ ≤ 1 := h.2.le
-              _ ≤ 2 * Real.pi - 1 := by rw [le_sub_iff_add_le]; linarith [Real.two_le_pi]
-              _ ≤ 2 * Real.pi - |x - y| := by gcongr; exact h.2.le
+              _ ≤ 2 * π - 1 := by rw [le_sub_iff_add_le]; linarith [Real.two_le_pi]
+              _ ≤ 2 * π - |x - y| := by gcongr; exact h.2.le
       _ = 2 / |x - y| := by rw [one_div, inv_div]
       _ ≤ (2 : ℝ) ^ (2 : ℝ) / (2 * |x - y|) := by ring_nf; trivial
   · push_neg at h
diff --git a/Carleson/Classical/VanDerCorput.lean b/Carleson/Classical/VanDerCorput.lean
index d53e9c6d..a9124ad3 100644
--- a/Carleson/Classical/VanDerCorput.lean
+++ b/Carleson/Classical/VanDerCorput.lean
@@ -3,12 +3,13 @@ import Carleson.Classical.Basic
 
 noncomputable section
 
+open scoped Real
 open Complex MeasureTheory
 
 lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B K: NNReal}
     (h1 : LipschitzWith K ϕ) (h2 : ∀ x ∈ (Set.Ioo a b), ‖ϕ x‖ ≤ B) :
     ‖∫ (x : ℝ) in a..b, (I * n * x).exp * ϕ x‖ ≤
-     2 * Real.pi * (b - a) * (B + K * (b - a) / 2) * (1 + |n| * (b - a))⁻¹ := by
+     2 * π * (b - a) * (B + K * (b - a) / 2) * (1 + |n| * (b - a))⁻¹ := by
   have hK : 0 ≤ K * (b - a) / 2 := by
     apply mul_nonneg (mul_nonneg (by simp) (by linarith)) (by norm_num)
   by_cases n_nonzero : n = 0
@@ -25,7 +26,7 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
         · exact Real.volume_Ioo ▸ ENNReal.ofReal_lt_top
       _ = B * (b - a) := by rw [Real.volume_Ioo, ENNReal.toReal_ofReal (by linarith)]
       _ = 1 * (b - a) * B := by ring
-      _ ≤ 2 * Real.pi * (b - a) * (↑B + ↑K * (b - a) / 2) := by
+      _ ≤ 2 * π * (b - a) * (↑B + ↑K * (b - a) / 2) := by
         gcongr
         · exact mul_nonneg Real.two_pi_pos.le (by linarith)
         · exact sub_nonneg_of_le hab
@@ -45,7 +46,7 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
         congr
         simp
         -- exact Or.inl (conj_ofReal _)
-      _ ≤ 2 * Real.pi * (b - a) * (↑B + ↑K * (b - a) / 2) * (1 + ↑|-n| * (b - a))⁻¹ := by
+      _ ≤ 2 * π * (b - a) * (↑B + ↑K * (b - a) / 2) * (1 + ↑|-n| * (b - a))⁻¹ := by
         apply this
         · intro x y
           simp only [Function.comp_apply]
@@ -58,7 +59,7 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
         · rw [Left.neg_pos_iff]; exact lt_of_le_of_ne n_pos n_nonzero
     rw [abs_neg]
   --Case distinction such that splitting integrals in the second case works.
-  by_cases h : b - a < Real.pi / n
+  by_cases h : b - a < π / n
   · have : 0 < 1 + ↑|n| * (b - a) := by
       apply add_pos_of_pos_of_nonneg zero_lt_one
       apply mul_nonneg (by simp) (by linarith)
@@ -77,7 +78,7 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
         rw [mul_inv_cancel₀]
         ring
         exact ne_of_gt this
-      _ ≤ (Real.pi + Real.pi) * (1 + |n| * (b - a))⁻¹ * (b - a) * (B + K * (b - a) / 2) := by
+      _ ≤ (π + π) * (1 + |n| * (b - a))⁻¹ * (b - a) * (B + K * (b - a) / 2) := by
         gcongr
         · apply mul_nonneg
           apply mul_nonneg
@@ -89,39 +90,39 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
         · rw [mul_comm, _root_.abs_of_nonneg n_pos.le]
           exact mul_le_of_nonneg_of_le_div Real.pi_pos.le (by exact_mod_cast n_pos.le) h.le
         · simpa
-      _ = 2 * Real.pi * (b - a) * (B + K * (b - a) / 2) * (1 + |n| * (b - a))⁻¹ := by ring
+      _ = 2 * π * (b - a) * (B + K * (b - a) / 2) * (1 + |n| * (b - a))⁻¹ := by ring
   push_neg at h
-  have pi_div_n_pos : 0 < Real.pi / n := div_pos Real.pi_pos (Int.cast_pos.mpr n_pos)
+  have pi_div_n_pos : 0 < π / n := div_pos Real.pi_pos (Int.cast_pos.mpr n_pos)
   have integrand_continuous : Continuous (fun x ↦ cexp (I * ↑n * ↑x) * ϕ x)  :=
     Continuous.mul (by continuity) h1.continuous
-  have integrand_continuous2 : Continuous (fun x ↦ cexp (I * ↑n * (↑x + ↑Real.pi / ↑n)) * ϕ x) :=
+  have integrand_continuous2 : Continuous (fun x ↦ cexp (I * ↑n * (↑x + ↑π / ↑n)) * ϕ x) :=
     Continuous.mul (by continuity) h1.continuous
-  have integrand_continuous3 : Continuous (fun (x : ℝ) ↦ cexp (I * n * x) * ϕ (x - Real.pi / n)) :=
+  have integrand_continuous3 : Continuous (fun (x : ℝ) ↦ cexp (I * n * x) * ϕ (x - π / n)) :=
     Continuous.mul (by continuity) (h1.continuous.comp (by continuity))
   calc _
-    _ = ‖∫ (x : ℝ) in a..b, (1 / 2 * (I * n * x).exp - 1 / 2 * (I * ↑n * (↑x + ↑Real.pi / ↑n)).exp) * ϕ x‖ := by
+    _ = ‖∫ (x : ℝ) in a..b, (1 / 2 * (I * n * x).exp - 1 / 2 * (I * ↑n * (↑x + ↑π / ↑n)).exp) * ϕ x‖ := by
       congr
       ext x
       congr
-      rw [mul_add, mul_assoc I n (Real.pi / n), mul_div_cancel₀ _ (by simpa), exp_add, mul_comm I Real.pi, exp_pi_mul_I]
+      rw [mul_add, mul_assoc I n (π / n), mul_div_cancel₀ _ (by simpa), exp_add, mul_comm I π, exp_pi_mul_I]
       ring
-    _ = ‖1 / 2 * ∫ (x : ℝ) in a..b, cexp (I * ↑n * ↑x) * ϕ x - cexp (I * ↑n * (↑x + ↑Real.pi / ↑n)) * ϕ x‖ := by
+    _ = ‖1 / 2 * ∫ (x : ℝ) in a..b, cexp (I * ↑n * ↑x) * ϕ x - cexp (I * ↑n * (↑x + ↑π / ↑n)) * ϕ x‖ := by
       congr
       rw [← intervalIntegral.integral_const_mul]
       congr
       ext x
       ring
-    _ = 1 / 2 * ‖(∫ (x : ℝ) in a..b, (I * n * x).exp * ϕ x) - (∫ (x : ℝ) in a..b, (I * n * (x + Real.pi / n)).exp * ϕ x)‖ := by
+    _ = 1 / 2 * ‖(∫ (x : ℝ) in a..b, (I * n * x).exp * ϕ x) - (∫ (x : ℝ) in a..b, (I * n * (x + π / n)).exp * ϕ x)‖ := by
       rw [norm_mul]
       congr
       simp
       rw [← intervalIntegral.integral_sub]
       · exact integrand_continuous.intervalIntegrable _ _
       · exact integrand_continuous2.intervalIntegrable _ _
-    _ = 1 / 2 * ‖  (∫ (x : ℝ) in a..(a + Real.pi / n), (I * n * x).exp * ϕ x)
-                 + (∫ (x : ℝ) in (a + Real.pi / n)..b, (I * n * x).exp * ϕ x)
-                 -((∫ (x : ℝ) in a..(b - Real.pi / n), (I * n * (x + Real.pi / n)).exp * ϕ x)
-                 + (∫ (x : ℝ) in (b - Real.pi / n)..b, (I * n * (x + Real.pi / n)).exp * ϕ x))‖ := by
+    _ = 1 / 2 * ‖  (∫ (x : ℝ) in a..(a + π / n), (I * n * x).exp * ϕ x)
+                 + (∫ (x : ℝ) in (a + π / n)..b, (I * n * x).exp * ϕ x)
+                 -((∫ (x : ℝ) in a..(b - π / n), (I * n * (x + π / n)).exp * ϕ x)
+                 + (∫ (x : ℝ) in (b - π / n)..b, (I * n * (x + π / n)).exp * ϕ x))‖ := by
       congr 3
       rw [intervalIntegral.integral_add_adjacent_intervals]
       · exact integrand_continuous.intervalIntegrable _ _
@@ -129,23 +130,23 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
       rw [intervalIntegral.integral_add_adjacent_intervals]
       · exact integrand_continuous2.intervalIntegrable _ _
       · exact integrand_continuous2.intervalIntegrable _ _
-    _ = 1 / 2 * ‖  (∫ (x : ℝ) in a..(a + Real.pi / n), (I * n * x).exp * ϕ x)
-                 + (∫ (x : ℝ) in (a + Real.pi / n)..b, (I * n * x).exp * ϕ x)
-                 -((∫ (x : ℝ) in (a + Real.pi / n)..(b - Real.pi / n + Real.pi / n), (I * n * x).exp * ϕ (x - Real.pi / n))
-                 + (∫ (x : ℝ) in (b - Real.pi / n)..b, (I * n * (x + Real.pi / n)).exp * ϕ x))‖ := by
+    _ = 1 / 2 * ‖  (∫ (x : ℝ) in a..(a + π / n), (I * n * x).exp * ϕ x)
+                 + (∫ (x : ℝ) in (a + π / n)..b, (I * n * x).exp * ϕ x)
+                 -((∫ (x : ℝ) in (a + π / n)..(b - π / n + π / n), (I * n * x).exp * ϕ (x - π / n))
+                 + (∫ (x : ℝ) in (b - π / n)..b, (I * n * (x + π / n)).exp * ϕ x))‖ := by
       congr 4
       rw [← intervalIntegral.integral_comp_add_right]
       simp
-    _ = 1 / 2 * ‖  (∫ (x : ℝ) in a..(a + Real.pi / n), (I * n * x).exp * ϕ x)
-                 +((∫ (x : ℝ) in (a + Real.pi / n)..b, (I * n * x).exp * ϕ x)
-                 - (∫ (x : ℝ) in (a + Real.pi / n)..b, (I * n * x).exp * ϕ (x - Real.pi / n)))
-                 - (∫ (x : ℝ) in (b - Real.pi / n)..b, (I * n * (x + Real.pi / n)).exp * ϕ x)‖ := by
+    _ = 1 / 2 * ‖  (∫ (x : ℝ) in a..(a + π / n), (I * n * x).exp * ϕ x)
+                 +((∫ (x : ℝ) in (a + π / n)..b, (I * n * x).exp * ϕ x)
+                 - (∫ (x : ℝ) in (a + π / n)..b, (I * n * x).exp * ϕ (x - π / n)))
+                 - (∫ (x : ℝ) in (b - π / n)..b, (I * n * (x + π / n)).exp * ϕ x)‖ := by
       congr 2
       rw [sub_add_cancel]
       ring
-    _ = 1 / 2 * ‖  (∫ (x : ℝ) in a..(a + Real.pi / n), (I * n * x).exp * ϕ x)
-                 + (∫ (x : ℝ) in (a + Real.pi / n)..b, (I * n * x).exp * (ϕ x - ϕ (x - Real.pi / n)))
-                 - (∫ (x : ℝ) in (b - Real.pi / n)..b, (I * n * (x + Real.pi / n)).exp * ϕ x)‖ := by
+    _ = 1 / 2 * ‖  (∫ (x : ℝ) in a..(a + π / n), (I * n * x).exp * ϕ x)
+                 + (∫ (x : ℝ) in (a + π / n)..b, (I * n * x).exp * (ϕ x - ϕ (x - π / n)))
+                 - (∫ (x : ℝ) in (b - π / n)..b, (I * n * (x + π / n)).exp * ϕ x)‖ := by
       congr 4
       rw [← intervalIntegral.integral_sub]
       congr
@@ -153,26 +154,26 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
       ring
       · exact integrand_continuous.intervalIntegrable _ _
       · exact integrand_continuous3.intervalIntegrable _ _
-    _ ≤ 1 / 2 * (  ‖(∫ (x : ℝ) in a..(a + Real.pi / n), (I * n * x).exp * ϕ x)
-                 +  (∫ (x : ℝ) in (a + Real.pi / n)..b, (I * n * x).exp * (ϕ x - ϕ (x - Real.pi / n)))‖
-                 + ‖∫ (x : ℝ) in (b - Real.pi / n)..b, (I * n * (x + Real.pi / n)).exp * ϕ x‖) := by
+    _ ≤ 1 / 2 * (  ‖(∫ (x : ℝ) in a..(a + π / n), (I * n * x).exp * ϕ x)
+                 +  (∫ (x : ℝ) in (a + π / n)..b, (I * n * x).exp * (ϕ x - ϕ (x - π / n)))‖
+                 + ‖∫ (x : ℝ) in (b - π / n)..b, (I * n * (x + π / n)).exp * ϕ x‖) := by
       gcongr
       exact norm_sub_le _ _
-    _ ≤ 1 / 2 * (  ‖(∫ (x : ℝ) in a..(a + Real.pi / n), (I * n * x).exp * ϕ x)‖
-                 + ‖(∫ (x : ℝ) in (a + Real.pi / n)..b, (I * n * x).exp * (ϕ x - ϕ (x - Real.pi / n)))‖
-                 + ‖∫ (x : ℝ) in (b - Real.pi / n)..b, (I * n * (x + Real.pi / n)).exp * ϕ x‖) := by
+    _ ≤ 1 / 2 * (  ‖(∫ (x : ℝ) in a..(a + π / n), (I * n * x).exp * ϕ x)‖
+                 + ‖(∫ (x : ℝ) in (a + π / n)..b, (I * n * x).exp * (ϕ x - ϕ (x - π / n)))‖
+                 + ‖∫ (x : ℝ) in (b - π / n)..b, (I * n * (x + π / n)).exp * ϕ x‖) := by
       gcongr
       exact norm_add_le _ _
-    _ = 1 / 2 * (  ‖∫ (x : ℝ) in Set.Ioo a (a + Real.pi / n), (I * n * x).exp * ϕ x‖
-                 + ‖∫ (x : ℝ) in Set.Ioo (a + Real.pi / n) b, (I * n * x).exp * (ϕ x - ϕ (x - Real.pi / n))‖
-                 + ‖∫ (x : ℝ) in Set.Ioo (b - Real.pi / n) b, (I * n * (x + Real.pi / n)).exp * ϕ x‖) := by
+    _ = 1 / 2 * (  ‖∫ (x : ℝ) in Set.Ioo a (a + π / n), (I * n * x).exp * ϕ x‖
+                 + ‖∫ (x : ℝ) in Set.Ioo (a + π / n) b, (I * n * x).exp * (ϕ x - ϕ (x - π / n))‖
+                 + ‖∫ (x : ℝ) in Set.Ioo (b - π / n) b, (I * n * (x + π / n)).exp * ϕ x‖) := by
       congr
       all_goals
         rw [intervalIntegral.integral_of_le, ← integral_Ioc_eq_integral_Ioo]
         linarith
-    _ ≤ 1 / 2 * (  B * (volume (Set.Ioo a (a + Real.pi / n))).toReal
-                 + (K * Real.pi / n) * (volume (Set.Ioo (a + Real.pi / n) b)).toReal
-                 + B * (volume (Set.Ioo (b - Real.pi / n) b)).toReal) := by
+    _ ≤ 1 / 2 * (  B * (volume (Set.Ioo a (a + π / n))).toReal
+                 + (K * π / n) * (volume (Set.Ioo (a + π / n) b)).toReal
+                 + B * (volume (Set.Ioo (b - π / n) b)).toReal) := by
       gcongr
       · apply norm_setIntegral_le_of_norm_le_const' _ measurableSet_Ioo
         · intro x hx
@@ -198,25 +199,25 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
           apply h2
           constructor <;> linarith [hx.1, hx.2]
         · exact Real.volume_Ioo ▸ ENNReal.ofReal_lt_top
-    _ = Real.pi / n * (B + K * (b - (a + Real.pi / n)) / 2) := by
+    _ = π / n * (B + K * (b - (a + π / n)) / 2) := by
       rw [Real.volume_Ioo, Real.volume_Ioo, Real.volume_Ioo, ENNReal.toReal_ofReal, ENNReal.toReal_ofReal, ENNReal.toReal_ofReal]
       ring
       all_goals linarith
-    _ ≤ Real.pi / n * (B + K * (b - a) / 2) := by
+    _ ≤ π / n * (B + K * (b - a) / 2) := by
       gcongr
       linarith
-    _ ≤ (2 * Real.pi / (1 + n * (b - a)) * (b - a)) * (B + K * (b - a) / 2) := by
+    _ ≤ (2 * π / (1 + n * (b - a)) * (b - a)) * (B + K * (b - a) / 2) := by
       gcongr
       rw [mul_comm, ← mul_div_assoc, div_le_div_iff (by simpa)]
-      calc Real.pi * (1 + n * (b - a))
-        _ ≤ Real.pi * (Real.pi + n * (b - a)) := by
+      calc π * (1 + n * (b - a))
+        _ ≤ π * (π + n * (b - a)) := by
           gcongr
           linarith [Real.two_le_pi]
-        _ ≤ Real.pi * (n * (b - a) + n * (b - a)) := by
+        _ ≤ π * (n * (b - a) + n * (b - a)) := by
           gcongr
           rwa [← div_le_iff₀' (Int.cast_pos.mpr n_pos)]
-        _ = (b - a) * (2 * Real.pi) * n := by ring
+        _ = (b - a) * (2 * π) * n := by ring
       exact add_pos zero_lt_one (mul_pos (Int.cast_pos.mpr n_pos) (gt_of_ge_of_gt h pi_div_n_pos))
-    _ = 2 * Real.pi * (b - a) * (B + K * (b - a) / 2) * (1 + |n| * (b - a))⁻¹ := by
+    _ = 2 * π * (b - a) * (B + K * (b - a) / 2) * (1 + |n| * (b - a))⁻¹ := by
       rw [_root_.abs_of_nonneg n_pos.le]
       ring
diff --git a/Carleson/Discrete/Defs.lean b/Carleson/Discrete/Defs.lean
index 8a7a7e5c..a898c489 100644
--- a/Carleson/Discrete/Defs.lean
+++ b/Carleson/Discrete/Defs.lean
@@ -51,7 +51,7 @@ def 𝔅 (k n : ℕ) (p : 𝔓 X) : Set (𝔓 X) :=
   { m ∈ 𝔐 k n | smul 100 p ≤ smul 1 m }
 
 def preℭ₁ (k n j : ℕ) : Set (𝔓 X) :=
-  { p ∈ ℭ k n | 2 ^ j ≤ (Finset.univ.filter (· ∈ 𝔅 k n p)).card }
+  { p ∈ ℭ k n | 2 ^ j ≤ Finset.card { q | q ∈ 𝔅 k n p } }
 
 /-- The subset `ℭ₁(k, n, j)` of `ℭ(k, n)`, given in (5.1.9).
 Together with `𝔏₀(k, n)` this forms a partition. -/
@@ -192,7 +192,7 @@ lemma measurable_setA {l k n : ℕ} : MeasurableSet (setA (X := X) l k n) :=
   measurableSet_lt measurable_const (Finset.measurable_sum _ fun _ _ ↦ measurable_one.indicator coeGrid_measurable)
 
 /-- Finset of cubes in `setA`. Appears in the proof of Lemma 5.2.5. -/
-def MsetA (l k n : ℕ) : Finset (Grid X) := Finset.univ.filter fun j ↦ (j : Set X) ⊆ setA l k n
+def MsetA (l k n : ℕ) : Finset (Grid X) := { j | (j : Set X) ⊆ setA l k n }
 
 /-- The set `G₂`, defined in (5.1.27). -/
 def G₂ : Set X := ⋃ (n : ℕ) (k ≤ n), setA (2 * n + 6) k n
diff --git a/Carleson/Discrete/ExceptionalSet.lean b/Carleson/Discrete/ExceptionalSet.lean
index 46af4126..3bd34abf 100644
--- a/Carleson/Discrete/ExceptionalSet.lean
+++ b/Carleson/Discrete/ExceptionalSet.lean
@@ -131,7 +131,7 @@ end first_exception
 /-- Lemma 5.2.2 -/
 lemma dense_cover (k : ℕ) : volume (⋃ i ∈ 𝓒 (X := X) k, (i : Set X)) ≤ 2 ^ (k + 1) * volume G := by
   let M : Finset (Grid X) :=
-    Finset.univ.filter fun j ↦ (2 ^ (-(k + 1 : ℕ) : ℤ) * volume (j : Set X) < volume (G ∩ j))
+    { j | 2 ^ (-(k + 1 : ℕ) : ℤ) * volume (j : Set X) < volume (G ∩ j) }
   have s₁ : ⋃ i ∈ 𝓒 (X := X) k, (i : Set X) ⊆ ⋃ i ∈ M, ↑i := by
     simp_rw [𝓒]; intro q mq; rw [mem_iUnion₂] at mq ⊢; obtain ⟨i, hi, mi⟩ := mq
     rw [aux𝓒, mem_diff, mem_setOf] at hi; obtain ⟨j, hj, mj⟩ := hi.1
@@ -173,7 +173,7 @@ lemma pairwiseDisjoint_E1 : (𝔐 (X := X) k n).PairwiseDisjoint E₁ := fun p m
 
 /-- Lemma 5.2.4 -/
 lemma dyadic_union (hx : x ∈ setA l k n) : ∃ i : Grid X, x ∈ i ∧ (i : Set X) ⊆ setA l k n := by
-  let M : Finset (𝔓 X) := Finset.univ.filter (fun p ↦ p ∈ 𝔐 k n ∧ x ∈ 𝓘 p)
+  let M : Finset (𝔓 X) := { p | p ∈ 𝔐 k n ∧ x ∈ 𝓘 p }
   simp_rw [setA, mem_setOf, stackSize, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_id,
     Finset.filter_filter] at hx ⊢
   obtain ⟨b, memb, minb⟩ := M.exists_min_image 𝔰 (Finset.card_pos.mp (zero_le'.trans_lt hx))
@@ -251,7 +251,7 @@ lemma john_nirenberg_aux1 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n))
 /-- Equation (5.2.11) in the proof of Lemma 5.2.5. -/
 lemma john_nirenberg_aux2 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n)) :
     2 * volume (setA (X := X) (l + 1) k n ∩ L) ≤ volume (L : Set X) := by
-  let Q₁ := Finset.univ.filter (fun q ↦ q ∈ 𝔐 (X := X) k n ∧ 𝓘 q ≤ L)
+  let Q₁ : Finset (𝔓 X) := { q | q ∈ 𝔐 (X := X) k n ∧ 𝓘 q ≤ L }
   have Q₁m : ∀ i ∈ Q₁, Measurable ((𝓘 i : Set X).indicator (1 : X → ℝ≥0∞)) := fun _ _ ↦
     measurable_one.indicator coeGrid_measurable
   have e528 : ∑ q ∈ Q₁, volume (E₁ q) ≤ volume (L : Set X) :=
@@ -382,7 +382,7 @@ section TopTiles
 
 /-- The volume of a "layer" in the key function of Lemma 5.2.7. -/
 def layervol (k n : ℕ) (t : ℝ) : ℝ≥0∞ :=
-  volume {x | t ≤ ∑ m ∈ Finset.univ.filter (· ∈ 𝔐 (X := X) k n),
+  volume {x | t ≤ ∑ m ∈ {p | p ∈ 𝔐 (X := X) k n },
     (𝓘 m : Set X).indicator (1 : X → ℝ) x}
 
 lemma indicator_sum_eq_natCast {s : Finset (𝔓 X)} :
@@ -429,16 +429,16 @@ lemma lintegral_Ioc_layervol_le {a b : ℕ} : ∫⁻ t in Ioc (a : ℝ) b, layer
       Finset.sum_le_sum fun l ml ↦ antitone_layervol (by simp_all)
     _ = _ := by rw [Finset.sum_const, Nat.card_Ico, nsmul_eq_mul]
 
-lemma top_tiles_aux : ∑ m ∈ Finset.univ.filter (· ∈ 𝔐 (X := X) k n), volume (𝓘 m : Set X) =
+lemma top_tiles_aux : ∑ m ∈ { p | p ∈ 𝔐 (X := X) k n }, volume (𝓘 m : Set X) =
     ∫⁻ t in Ioc 0 ((𝔐 (X := X) k n).toFinset.card * 2 ^ (n + 1) : ℝ), layervol (X := X) k n t := by
   set M := 𝔐 (X := X) k n
   set Mc := M.toFinset.card
   calc
-    _ = ∑ m ∈ Finset.univ.filter (· ∈ M), ∫⁻ x, (𝓘 m : Set X).indicator 1 x := by
+    _ = ∑ m ∈ { p | p ∈ M }, ∫⁻ x, (𝓘 m : Set X).indicator 1 x := by
       congr! with m; exact (lintegral_indicator_one coeGrid_measurable).symm
-    _ = ∫⁻ x, ∑ m ∈ Finset.univ.filter (· ∈ M), (𝓘 m : Set X).indicator 1 x :=
+    _ = ∫⁻ x, ∑ m ∈ { p | p ∈ M }, (𝓘 m : Set X).indicator 1 x :=
       (lintegral_finset_sum _ fun _ _ ↦ measurable_one.indicator coeGrid_measurable).symm
-    _ = ∫⁻ x, ENNReal.ofReal (∑ m ∈ Finset.univ.filter (· ∈ M), (𝓘 m : Set X).indicator 1 x) := by
+    _ = ∫⁻ x, ENNReal.ofReal (∑ m ∈ { p | p ∈ M }, (𝓘 m : Set X).indicator 1 x) := by
       congr! 2 with x; rw [ENNReal.ofReal_sum_of_nonneg]
       · congr!; unfold indicator; split_ifs <;> simp
       · exact fun _ _ ↦ indicator_nonneg (fun _ _ ↦ by simp) _
@@ -460,7 +460,7 @@ lemma top_tiles_aux : ∑ m ∈ Finset.univ.filter (· ∈ 𝔐 (X := X) k n), v
       rw [cgr, lintegral_zero]
 
 /-- Lemma 5.2.7 -/
-lemma top_tiles : ∑ m ∈ Finset.univ.filter (· ∈ 𝔐 (X := X) k n), volume (𝓘 m : Set X) ≤
+lemma top_tiles : ∑ m ∈ { p | p ∈ 𝔐 (X := X) k n }, volume (𝓘 m : Set X) ≤
     2 ^ (n + k + 3) * volume G := by
   set M := 𝔐 (X := X) k n
   let Mc := M.toFinset.card
@@ -665,16 +665,16 @@ lemma third_exception_aux :
       measure_biUnion_le _ (𝔘₁ k n j).to_countable _
     _ ≤ ∑' u : 𝔘₁ (X := X) k n j, C5_2_9 X n * volume (𝓘 u.1 : Set X) :=
       ENNReal.tsum_le_tsum fun x ↦ boundary_exception x.2
-    _ = C5_2_9 X n * ∑ u ∈ Finset.univ.filter (· ∈ 𝔘₁ (X := X) k n j), volume (𝓘 u : Set X) := by
+    _ = C5_2_9 X n * ∑ u ∈ { p | p ∈ 𝔘₁ (X := X) k n j }, volume (𝓘 u : Set X) := by
       rw [filter_mem_univ_eq_toFinset, ENNReal.tsum_mul_left]; congr
       rw [tsum_fintype]; convert (Finset.sum_subtype _ (fun u ↦ mem_toFinset) _).symm; rfl
     _ ≤ C5_2_9 X n * 2 ^ (9 * a - j : ℤ) *
-        ∑ m ∈ Finset.univ.filter (· ∈ 𝔐 (X := X) k n), volume (𝓘 m : Set X) := by
+        ∑ m ∈ { p | p ∈ 𝔐 (X := X) k n }, volume (𝓘 m : Set X) := by
       rw [mul_assoc]; refine mul_le_mul_left' ?_ _
       simp_rw [← lintegral_indicator_one coeGrid_measurable,
         ← lintegral_finset_sum _ fun _ _ ↦ measurable_one.indicator coeGrid_measurable]
       have c1 : ∀ C : Set (𝔓 X),
-          ∫⁻ x, ∑ u ∈ Finset.univ.filter (· ∈ C), (𝓘 u : Set X).indicator 1 x =
+          ∫⁻ x, ∑ u ∈ { p | p ∈ C }, (𝓘 u : Set X).indicator 1 x =
           ∫⁻ x, stackSize C x := fun C ↦ by
         refine lintegral_congr fun _ ↦ ?_; rw [stackSize, Nat.cast_sum]; congr!
         simp_rw [indicator]; split_ifs <;> simp
diff --git a/Carleson/Discrete/Forests.lean b/Carleson/Discrete/Forests.lean
index cf9e4c5a..80f89116 100644
--- a/Carleson/Discrete/Forests.lean
+++ b/Carleson/Discrete/Forests.lean
@@ -519,7 +519,7 @@ lemma stackSize_𝔘₃_le_𝔐 (x : X) : stackSize (𝔘₃ k n j) x ≤ stackS
 /-- Lemma 5.4.8, used to verify that 𝔘₄ satisfies 2.0.34. -/
 lemma forest_stacking (x : X) (hkn : k ≤ n) : stackSize (𝔘₃ (X := X) k n j) x ≤ C5_4_8 n := by
   by_contra! h
-  let C : Finset (𝔓 X) := Finset.univ.filter fun u ↦ u ∈ 𝔘₃ (X := X) k n j ∧ x ∈ 𝓘 u
+  let C : Finset (𝔓 X) := { u | u ∈ 𝔘₃ (X := X) k n j ∧ x ∈ 𝓘 u }
   have Cc : C.card = stackSize (𝔘₃ k n j) x := by
     simp_rw [stackSize, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_id,
       C, Grid.mem_def, Finset.filter_filter]
@@ -602,7 +602,7 @@ def C5_1_2 (a : ℝ) (q : ℝ≥0) : ℝ≥0 := 2 ^ (235 * a ^ 3) / (q - 1) ^ 4
 lemma C5_1_2_pos : C5_1_2 a nnq > 0 := sorry
 
 lemma forest_union {f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
-  ∫⁻ x in G \ G', ‖∑ p ∈ Finset.univ.filter (· ∈ 𝔓₁), carlesonOn p f x‖₊ ≤
+  ∫⁻ x in G \ G', ‖∑ p ∈ { p | p ∈ 𝔓₁ }, carlesonOn p f x‖₊ ≤
     C5_1_2 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹  := by
   sorry
 
@@ -742,10 +742,10 @@ lemma exists_k_n_j_of_mem_𝔓pos (h : p ∈ 𝔓pos (X := X)) :
     h.trans_le (measure_mono (inter_subset_left.trans inter_subset_left))
   obtain ⟨x, mx, nx⟩ := nonempty_of_measure_ne_zero h.ne'
   simp_rw [G₂, mem_compl_iff, mem_iUnion] at nx; push_neg at nx; specialize nx n k hkn
-  let B : ℕ := (Finset.univ.filter (· ∈ 𝔅 k n p)).card
+  let B : ℕ := Finset.card { q | q ∈ 𝔅 k n p }
   have Blt : B < 2 ^ (2 * n + 4) := by
     calc
-      _ ≤ (Finset.univ.filter fun m ↦ m ∈ 𝔐 k n ∧ x ∈ 𝓘 m).card :=
+      _ ≤ Finset.card { m | m ∈ 𝔐 k n ∧ x ∈ 𝓘 m } :=
         Finset.card_le_card (Finset.monotone_filter_right _ (Pi.le_def.mpr fun m ⟨m₁, m₂⟩ ↦
           ⟨m₁, m₂.1.1 mx⟩))
       _ = stackSize (𝔐 k n) x := by
@@ -849,7 +849,7 @@ lemma antichain_L2 : IsAntichain (· ≤ ·) (𝔏₂ (X := X) k n j) := by
         refine smul_C2_1_2 _ (by norm_num) ?_ (wiggle_order_11_10 l.le (C5_3_3_le (X := X)))
         apply not_lt_of_𝓘_eq_𝓘.mt; rwa [not_not]
   have cp : p ∈ ℭ₁ k n j := (𝔏₂_subset_ℭ₂.trans ℭ₂_subset_ℭ₁) mp
-  let C : Finset (LTSeries (ℭ₁' k n j)) := Finset.univ.filter fun s ↦ s.head = ⟨p, cp⟩
+  let C : Finset (LTSeries (ℭ₁' k n j)) := { s | s.head = ⟨p, cp⟩ }
   have Cn : C.Nonempty := by
     use RelSeries.singleton _ ⟨p, cp⟩
     simp_rw [C, Finset.mem_filter, Finset.mem_univ, true_and]; rfl
@@ -898,7 +898,7 @@ def C5_1_3 (a : ℝ) (q : ℝ≥0) : ℝ≥0 := 2 ^ (210 * a ^ 3) / (q - 1) ^ 5
 lemma C5_1_3_pos : C5_1_3 a nnq > 0 := sorry
 
 lemma forest_complement {f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
-  ∫⁻ x in G \ G', ‖∑ p ∈ Finset.univ.filter (· ∉ 𝔓₁), carlesonOn p f x‖₊ ≤
+  ∫⁻ x in G \ G', ‖∑ p ∈ { p | p ∉ 𝔓₁ }, carlesonOn p f x‖₊ ≤
     C5_1_2 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹  := by
   sorry
 
diff --git a/Carleson/FinitaryCarleson.lean b/Carleson/FinitaryCarleson.lean
index fd7cca22..8719216b 100644
--- a/Carleson/FinitaryCarleson.lean
+++ b/Carleson/FinitaryCarleson.lean
@@ -62,7 +62,7 @@ lemma exists_Grid {x : X} (hx : x ∈ G) {s : ℤ} (hs : s ∈ (Icc (σ₁ x) (
   simpa only [mem_iUnion, exists_prop] using Grid_subset_biUnion s s_mem x_mem_topCube
 
 /-- Lemma 4.0.3 -/
-theorem tile_sum_operator {G' : Set X} {f : X → ℂ} (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x)
+theorem tile_sum_operator {G' : Set X} {f : X → ℂ}
     {x : X} (hx : x ∈ G \ G') : ∑ (p : 𝔓 X), carlesonOn p f x =
     ∑ s in Icc (σ₁ x) (σ₂ x), ∫ y, Ks s x y * f y * exp (I * (Q x y - Q x x)) := by
   rw [𝔓_biUnion, Finset.sum_biUnion]; swap
@@ -111,7 +111,7 @@ theorem finitary_carleson : ∃ G', MeasurableSet G' ∧ 2 * volume G' ≤ volum
   rcases discrete_carleson X with ⟨G', hG', h2G', hfG'⟩
   refine ⟨G', hG', h2G', fun f meas_f h2f ↦ le_of_eq_of_le ?_ (hfG' f meas_f h2f)⟩
   refine setLIntegral_congr_fun (measurableSet_G.diff hG') (ae_of_all volume fun x hx ↦ ?_)
-  simp_rw [tile_sum_operator h2f hx, mul_sub, exp_sub, mul_div, div_eq_mul_inv,
+  simp_rw [tile_sum_operator hx, mul_sub, exp_sub, mul_div, div_eq_mul_inv,
     ← smul_eq_mul (a' := _⁻¹), integral_smul_const, ← Finset.sum_smul, nnnorm_smul]
   suffices ‖(cexp (I * ((Q x) x : ℂ)))⁻¹‖₊ = 1 by rw [this, mul_one]
   simp [← coe_eq_one, mul_comm I]
diff --git a/Carleson/Forest.lean b/Carleson/Forest.lean
index 33994702..53e87b45 100644
--- a/Carleson/Forest.lean
+++ b/Carleson/Forest.lean
@@ -12,7 +12,7 @@ variable [TileStructure Q D κ S o] {p p' : 𝔓 X} {f g : Θ X}
 
 /-- The number of tiles `p` in `s` whose underlying cube `𝓘 p` contains `x`. -/
 def stackSize (C : Set (𝔓 X)) (x : X) : ℕ :=
-  ∑ p ∈ Finset.univ.filter (· ∈ C), (𝓘 p : Set X).indicator 1 x
+  ∑ p ∈ { p | p ∈ C }, (𝓘 p : Set X).indicator 1 x
 
 lemma stackSize_setOf_add_stackSize_setOf_not {P : 𝔓 X → Prop} :
     stackSize {p ∈ C | P p} x + stackSize {p ∈ C | ¬ P p} x = stackSize C x := by
@@ -34,7 +34,7 @@ lemma stackSize_mono (h : C ⊆ C') : stackSize C x ≤ stackSize C' x := by
 
 -- Simplify the cast of `stackSize C x` from `ℕ` to `ℝ`
 lemma stackSize_real (C : Set (𝔓 X)) (x : X) : (stackSize C x : ℝ) =
-    ∑ p ∈ Finset.univ.filter (· ∈ C), (𝓘 p : Set X).indicator (1 : X → ℝ) x := by
+    ∑ p ∈ { p | p ∈ C }, (𝓘 p : Set X).indicator (1 : X → ℝ) x := by
   rw [stackSize, Nat.cast_sum]
   refine Finset.sum_congr rfl (fun u _ ↦ ?_)
   by_cases hx : x ∈ (𝓘 u : Set X) <;> simp [hx]
diff --git a/Carleson/ForestOperator.lean b/Carleson/ForestOperator.lean
index 00123a41..96c04b06 100644
--- a/Carleson/ForestOperator.lean
+++ b/Carleson/ForestOperator.lean
@@ -4,7 +4,7 @@ import Carleson.HardyLittlewood
 open ShortVariables TileStructure
 variable {X : Type*} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X}
   [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q D κ S o]
-  {n : ℕ} {t : Forest X n} {u : 𝔓 X} {x x' : X} {G : Set (𝔓 X)} {f : X → ℂ}
+  {n : ℕ} {t : Forest X n} {u : 𝔓 X} {x x' : X} {G : Set (𝔓 X)} {f g : X → ℂ}
   {I J L : Grid X}
 variable {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E']
 
@@ -20,12 +20,12 @@ namespace TileStructure.Forest
 variable (t) in
 /-- The definition `σ(u, x)` given in Section 7.1.
 We may assume `u ∈ t.𝔘` whenever proving things about this definition. -/
-def σ (u : 𝔓 X) (x : X) : Finset ℤ := Finset.univ.filter (fun p ↦ p ∈ t.𝔗 u ∧ x ∈ E p) |>.image 𝔰
+def σ (u : 𝔓 X) (x : X) : Finset ℤ := .image 𝔰 { p | p ∈ t.𝔗 u ∧ x ∈ E p }
 
 /- Maybe we should try to avoid using \overline{σ} and \underline{σ} in Lean:
 I don't think the set is always non-empty(?) -/
 -- def σMax (u : 𝔓 X) (x : X) : ℤ :=
---   Finset.univ.filter (fun p ↦ p ∈ t.𝔗 u ∧ x ∈ E p) |>.image 𝔰 |>.max' sorry
+--  Finset.image 𝔰 { p | p ∈ t.𝔗 u ∧ x ∈ E p } |>.max' sorry
 
 /-- Lemma 7.1.1, freely translated. -/
 lemma convex_scales (hu : u ∈ t.𝔘) : OrdConnected (t.σ u x : Set ℤ) := sorry
@@ -67,7 +67,7 @@ lemma pairwiseDisjoint_𝓛 : (𝓛 G).PairwiseDisjoint (fun I ↦ (I : Set X))
 /-- The projection operator `P_𝓒 f(x)`, given above Lemma 7.1.3.
 In lemmas the `c` will be pairwise disjoint on `C`. -/
 def approxOnCube (C : Set (Grid X)) (f : X → E') (x : X) : E' :=
-  ∑ J ∈ Finset.univ.filter (· ∈ C), (J : Set X).indicator (fun _ ↦ ⨍ y, f y) x
+  ∑ J ∈ { p | p ∈ C }, (J : Set X).indicator (fun _ ↦ ⨍ y, f y) x
 
 /-- The definition `I_i(x)`, given above Lemma 7.1.3.
 The cube of scale `s` that contains `x`. There is at most 1 such cube, if it exists. -/
@@ -84,10 +84,9 @@ def nontangentialMaximalFunction (θ : Θ X) (f : X → ℂ) (x : X) : ℝ≥0
 
 variable (t) in
 /-- The operator `S_{1,𝔲} f(x)`, given in (7.1.4). -/
-def auxiliaryOperator1 (u : 𝔓 X) (f : X → ℝ) (x : X) : ℝ≥0∞ :=
+def boundaryOperator1 (u : 𝔓 X) (f : X → ℂ) (x : X) : ℝ≥0∞ :=
   ∑ I : Grid X, (I : Set X).indicator (x := x) fun _ ↦
-  ∑ J ∈ Finset.univ.filter fun J ↦
-    J ∈ 𝓙 (t.𝔗 u) ∧ (J : Set X) ⊆ ball (c I) (16 * D ^ (s I)) ∧ s J ≤ s I,
+  ∑ J ∈ { J | J ∈ 𝓙 (t.𝔗 u) ∧ (J : Set X) ⊆ ball (c I) (16 * D ^ (s I)) ∧ s J ≤ s I },
   D ^ ((s J - s I) / a) / volume (ball (c I) (16 * D ^ (s I))) * ∫⁻ y in J, ‖f y‖₊
 
 /-- The indexing set for the collection of balls 𝓑, defined above Lemma 7.1.3. -/
@@ -126,7 +125,7 @@ def C7_1_6 (a : ℕ) : ℝ≥0 := 2 ^ (151 * (a : ℝ) ^ 3)
 lemma third_tree_pointwise (hu : u ∈ t.𝔘) (hL : L ∈ 𝓛 (t.𝔗 u)) (hx : x ∈ L) (hx' : x' ∈ L)
     (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
     ‖∑ i in t.σ u x, ∫ y, Ks i x y * (f y - approxOnCube (𝓙 (t.𝔗 u)) f y)‖₊ ≤
-    C7_1_6 a * t.auxiliaryOperator1 u (approxOnCube (𝓙 (t.𝔗 u)) (‖f ·‖)) x' := by
+    C7_1_6 a * t.boundaryOperator1 u (approxOnCube (𝓙 (t.𝔗 u)) (‖f ·‖)) x' := by
   sorry
 
 /-- The constant used in `pointwise_tree_estimate`.
@@ -137,9 +136,9 @@ def C7_1_3 (a : ℕ) : ℝ≥0 := 2 ^ (151 * (a : ℝ) ^ 3)
 /-- Lemma 7.1.3. -/
 lemma pointwise_tree_estimate (hu : u ∈ t.𝔘) (hL : L ∈ 𝓛 (t.𝔗 u)) (hx : x ∈ L) (hx' : x' ∈ L)
     (hf : IsBounded (range f)) (h2f : HasCompactSupport f) :
-    ‖∑ p ∈ Finset.univ.filter (· ∈ t.𝔗 u), carlesonOn p (fun y ↦ exp (.I * - 𝒬 u y) * f y) x‖₊ ≤
+    ‖∑ p ∈ { p | p ∈ t.𝔗 u }, carlesonOn p (fun y ↦ exp (.I * - 𝒬 u y) * f y) x‖₊ ≤
     C7_1_3 a * (MB volume 𝓑 (c ·.2) r𝓑 (approxOnCube (𝓙 (t.𝔗 u)) (‖f ·‖)) x' +
-    t.auxiliaryOperator1 u (approxOnCube (𝓙 (t.𝔗 u)) (‖f ·‖)) x' +
+    t.boundaryOperator1 u (approxOnCube (𝓙 (t.𝔗 u)) (‖f ·‖)) x' +
     nontangentialMaximalFunction (𝒬 u) (approxOnCube (𝓙 (t.𝔗 u)) f) x'):= by
   set g := approxOnCube (𝓙 (t.𝔗 u)) (‖f ·‖)
   sorry
@@ -147,7 +146,42 @@ lemma pointwise_tree_estimate (hu : u ∈ t.𝔘) (hL : L ∈ 𝓛 (t.𝔗 u)) (
 
 /-! ## Section 7.2 and Lemma 7.2.1 -/
 
-/- todo: make the argument `a` a natural number to constants everywhere(?) -/
+/-- The constant used in `nontangential_operator_bound`.
+Has value `2 ^ (103 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_2_2 (a : ℕ) : ℝ≥0 := 2 ^ (103 * (a : ℝ) ^ 3)
+
+/-- Lemma 7.2.2. -/
+lemma nontangential_operator_bound
+  (hf : IsBounded (range f)) (h2f : HasCompactSupport f) (θ : Θ X) :
+    eLpNorm (nontangentialMaximalFunction θ f · |>.toReal) 2 volume ≤ eLpNorm f 2 volume := by
+  sorry
+
+/-- Lemma 7.2.4. -/
+lemma boundary_overlap (I : Grid X) :
+    Finset.card { J | s J = s I ∧ ¬ Disjoint (ball (c I) (4 * D ^ s I)) (ball (c J) (4 * D ^ s J)) }
+    ≤ 2 ^ (9 * a) := by
+  sorry
+
+/-- Lemma 7.2.3. -/
+lemma boundary_operator_bound
+  (hf : IsBounded (range f)) (h2f : HasCompactSupport f) {u : 𝔓 X} (hu : u ∈ t.𝔘) :
+    eLpNorm (boundaryOperator1 t u f · |>.toReal) 2 volume ≤ eLpNorm f 2 volume := by
+  sorry
+
+/-- The constant used in `nontangential_operator_bound`.
+Has value `2 ^ (104 * a ^ 3)` in the blueprint. -/
+-- Todo: define this recursively in terms of previous constants
+def C7_2_1 (a : ℕ) : ℝ≥0 := 2 ^ (104 * (a : ℝ) ^ 3)
+
+/-- Lemma 7.2.1. -/
+lemma tree_projection_estimate
+  (hf : IsBounded (range f)) (h2f : HasCompactSupport f)
+  (hg : IsBounded (range g)) (h2g : HasCompactSupport g) {u : 𝔓 X} (hu : u ∈ t.𝔘) :
+    ‖∫ x, ∑ p ∈ t.𝔗 u, conj (g x) * carlesonOn p f x‖₊ ≤
+    C7_2_1 a * eLpNorm (approxOnCube (𝓙 (t.𝔗 u)) (‖f ·‖)) 2 volume *
+    eLpNorm (approxOnCube (𝓛 (t.𝔗 u)) (‖g ·‖)) 2 volume := by
+  sorry
 
 /-! ## Section 7.3 and Lemma 7.3.1 -/
 
@@ -185,8 +219,8 @@ def C2_0_4 (a q : ℝ) (n : ℕ) : ℝ≥0 := 2 ^ (432 * a ^ 3 - (q - 1) / q * n
 theorem forest_operator {n : ℕ} (𝔉 : Forest X n) {f g : X → ℂ}
     (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hg : Measurable g)
     (h2g : IsBounded (support g)) :
-    ‖∫ x, conj (g x) * ∑ u ∈ Finset.univ.filter (· ∈ 𝔉.𝔘),
-      ∑ p ∈ Finset.univ.filter (· ∈ 𝔉.𝔗 u), carlesonOn p f x‖₊ ≤
+    ‖∫ x, conj (g x) * ∑ u ∈ { p | p ∈ 𝔉.𝔘 },
+      ∑ p ∈ { p | p ∈ 𝔉.𝔗 u }, carlesonOn p f x‖₊ ≤
     C2_0_4 a q n * (dens₂ (X := X) (⋃ u ∈ 𝔉.𝔘, 𝔉.𝔗 u)) ^ (q⁻¹ - 2⁻¹) *
     eLpNorm f 2 volume * eLpNorm g 2 volume := by
   sorry
diff --git a/Carleson/GridStructure.lean b/Carleson/GridStructure.lean
index 502d9b75..557525c4 100644
--- a/Carleson/GridStructure.lean
+++ b/Carleson/GridStructure.lean
@@ -160,7 +160,7 @@ lemma le_dyadic {i j k : Grid X} (h : s i ≤ s j) (li : k ≤ i) (lj : k ≤ j)
 lemma exists_unique_succ (i : Grid X) (h : ¬IsMax i) :
     ∃! j ∈ Finset.univ, i < j ∧ ∀ j', i < j' → j ≤ j' := by
   simp_rw [Finset.mem_univ, true_and]
-  classical let incs : Finset (Grid X) := Finset.univ.filter (i < ·)
+  classical let incs : Finset (Grid X) := { j | i < j }
   have ine : incs.Nonempty := by
     use topCube; simp only [incs, Finset.mem_filter, Finset.mem_univ, true_and]
     exact lt_of_le_of_ne le_topCube (isMax_iff.not.mp h)
diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex
index 11c2328d..341393ca 100644
--- a/blueprint/src/chapter/main.tex
+++ b/blueprint/src/chapter/main.tex
@@ -4467,6 +4467,8 @@ \section{An auxiliary \texorpdfstring{$L^2$}{L2} tree estimate}
 
 \begin{lemma}[tree projection estimate]
     \label{tree-projection-estimate}
+    \leanok
+    \lean{TileStructure.Forest.tree_projection_estimate}
     \uses{dyadic-partitions,pointwise-tree-estimate,nontangential-operator-bound,boundary-operator-bound}
     Let $\fu \in \fU$.
     Then we have for all $f, g$ bounded with bounded support
@@ -4484,7 +4486,9 @@ \section{An auxiliary \texorpdfstring{$L^2$}{L2} tree estimate}
 
 \begin{lemma}[nontangential operator bound]
     \label{nontangential-operator-bound}
-  \uses{Hardy-Littlewood}
+    \leanok
+    \lean{TileStructure.Forest.nontangential_operator_bound}
+    \uses{Hardy-Littlewood}
     For all bounded $f$ with bounded supportand all $\mfa \in \Mf$
     $$
         \|T_{\mathcal{N}}^{\mfa} f\|_2 \le 2^{103a^3} \|f\|_2\,.
@@ -4493,6 +4497,8 @@ \section{An auxiliary \texorpdfstring{$L^2$}{L2} tree estimate}
 
 \begin{lemma}[boundary operator bound]
     \label{boundary-operator-bound}
+    \leanok
+    \lean{TileStructure.Forest.boundary_operator_bound}
     \uses{Hardy-Littlewood,boundary-overlap}
     For all $\fu \in \fU$ and all bounded functions $f$ with bounded support
     \begin{equation}
@@ -4678,6 +4684,8 @@ \section{An auxiliary \texorpdfstring{$L^2$}{L2} tree estimate}
 
 \begin{lemma}[boundary overlap]
     \label{boundary-overlap}
+    \leanok
+    \lean{TileStructure.Forest.boundary_overlap}
     For every cube $I \in \mathcal{D}$, there exist at most $2^{9a}$ cubes $J \in \mathcal{D}$ with $s(J) = s(I)$ and $B(c(I), 16D^{s(I)}) \cap B(c(J), 16 D^{s(J)}) \ne \emptyset$.
 \end{lemma}