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

@@ -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` |     |
 | ``        | `` |     |
 | ``        | `` |     |
 | ``        | `` |     |

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,26 +112,26 @@ 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) _
   /-Get better representation for the fourier coefficients of f. -/
   have fourierCoeffOn_eq {n : ℤ} (hn : n ≠ 0): (fourierCoeffOn Real.two_pi_pos f n) = - 1 / (n^2) * fourierCoeffOn Real.two_pi_pos (fun x ↦ deriv (deriv f) x) n := by
     rw [fourierCoeffOn_of_hasDerivAt Real.two_pi_pos hn h, fourierCoeffOn_of_hasDerivAt Real.two_pi_pos hn h']
     · 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]

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,21 +188,21 @@ 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
     _ ≤ 0 := by linarith
     _ ≤ ‖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]