Update blueprint section 10 (#22)

Carleson/Theorem1_1/Approximation.lean

@@ -37,7 +37,6 @@ lemma uniformContinuous_iff_bounded [PseudoMetricSpace α] [PseudoMetricSpace β
   . intro h ε εpos
     obtain ⟨δ, δpos, _, hδ⟩ := h ε εpos
     use δ
-
 end section
 
 /- TODO: might be generalized. -/
@@ -296,7 +295,7 @@ lemma int_sum_nat {β : Type} [AddCommGroup β] [TopologicalSpace β] [Continuou
 
 /-TODO: Weaken statement to pointwise convergence to simplify proof?-/
 lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : Function.Periodic f (2 * Real.pi)) (fdiff : ContDiff ℝ 2 f) {ε : ℝ} (εpos : ε > 0) :
-    ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Ico 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε := by
+    ∃ N₀, ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f x - partialFourierSum f N x) ≤ ε := by
   have fact_two_pi_pos : Fact (0 < 2 * Real.pi) := by
     rw [fact_iff]
     exact Real.two_pi_pos
@@ -343,11 +342,19 @@ lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : Function.
   simp only [ContinuousMap.coe_sum, sum_apply] at this
   convert this.le using 2
   congr 1
-  . rw [g_def]
-    simp only [ContinuousMap.coe_mk]
-    rw [AddCircle.liftIco_coe_apply]
-    rw [zero_add]
-    exact hx
+  . 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
+      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
+        use hx.1
+        apply lt_of_le_of_ne hx.2 h
+      rw [AddCircle.liftIco_coe_apply]
+      rw [zero_add]
+      exact this
   . rw [partialFourierSum]
     congr
     ext n

Carleson/Theorem1_1/Basic.lean

@@ -102,12 +102,17 @@ lemma partialFourierSum_uniformContinuous {f : ℝ → ℂ} {N : ℕ} : UniformC
   sorry
 
 
-/-Slightly different and stronger version of Lemma 10.11 (lower secant bound). -/
+theorem strictConvexOn_cos_Icc : StrictConvexOn ℝ (Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 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 10.11 (lower secant bound) from the paper. -/
 lemma lower_secant_bound' {η : ℝ}  {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_le : |x| ≤ 2 * Real.pi - η) :
-    η / 4 ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by
+    (2 / Real.pi) * η ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by
   by_cases ηpos : η ≤ 0
-  . calc η / 4
-    _ ≤ 0 := by linarith
+  . calc (2 / Real.pi) * η
+    _ ≤ 0 := mul_nonpos_of_nonneg_of_nonpos (div_nonneg zero_le_two Real.pi_pos.le) ηpos
     _ ≤ ‖1 - Complex.exp (Complex.I * x)‖ := by apply norm_nonneg
   push_neg at ηpos
   wlog x_nonneg : 0 ≤ x generalizing x
@@ -125,13 +130,7 @@ lemma lower_secant_bound' {η : ℝ}  {x : ℝ} (le_abs_x : η ≤ |x|) (abs_x_l
       rw [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]
     all_goals linarith
   by_cases h : x ≤ Real.pi / 2
-  . calc η / 4
-    _ ≤ (2 / Real.pi) * η := by
-      rw [div_le_iff (by norm_num)]
-      field_simp
-      rw [le_div_iff Real.pi_pos, mul_comm 2, mul_assoc]
-      gcongr
-      linarith [Real.pi_le_four]
+  . 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
@@ -156,30 +155,52 @@ 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 η / 4
-    _ ≤ 1 := by
-      rw [div_le_iff (by norm_num), one_mul]
-      exact (le_abs_x.trans x_le_pi).trans Real.pi_le_four
-    _ ≤ |(1 - Complex.exp (Complex.I * ↑x)).re| := by
-      rw [mul_comm, Complex.exp_mul_I]
-      simp
-      rw [Complex.cos_ofReal_re, le_abs]
-      left
-      simp
-      apply Real.cos_nonpos_of_pi_div_two_le_of_le h.le
-      linarith
+    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
+      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
+      gcongr
+      apply (strictConvexOn_cos_Icc.convexOn).2 (by simp [Real.pi_nonneg])
+      . simp
+        constructor <;> linarith [Real.pi_nonneg]
+      . rw [sub_nonneg, mul_comm]
+        apply 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])
+      . simp
+    _ = 1 - Real.cos x := by
+      congr
+      field_simp
+      ring
+    _ ≤ Real.sqrt ((1 - Real.cos x) ^ 2) := by
+      rw [Real.sqrt_sq_eq_abs]
+      apply le_abs_self
     _ ≤ ‖1 - Complex.exp (Complex.I * ↑x)‖ := by
-      rw [Complex.norm_eq_abs]
-      apply Complex.abs_re_le_abs
+        rw [mul_comm, Complex.exp_mul_I, Complex.norm_eq_abs, Complex.abs_eq_sqrt_sq_add_sq]
+        simp
+        rw [Complex.cos_ofReal_re, Complex.sin_ofReal_re]
+        apply (Real.sqrt_le_sqrt_iff _).mpr
+        . simp [pow_two_nonneg]
+        . linarith [pow_two_nonneg (1 - Real.cos x), pow_two_nonneg (Real.sin x)]
 
-/- Lemma 10.11 (lower secant bound) from the paper. -/
-lemma lower_secant_bound {η : ℝ} (ηpos : η > 0) {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)) (xAbs : η ≤ |x|) :
-    η / 8 ≤ Complex.abs (1 - Complex.exp (Complex.I * x)) := by
-  calc η / 8
-  _ ≤ η / 4 := by
+
+/-Slightly weaker version of Lemma 10.11 (lower secant bound) with simplified constant. -/
+lemma lower_secant_bound {η : ℝ} {x : ℝ} (xIcc : x ∈ Set.Icc (-2 * Real.pi + η) (2 * Real.pi - η)) (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)‖ := by apply norm_nonneg
+  push_neg at ηpos
+  calc η / 2
+  _ ≤ (2 / Real.pi) * η := by
     ring_nf
+    rw [mul_assoc]
     gcongr
-    norm_num
+    field_simp
+    rw [div_le_div_iff (by norm_num) Real.pi_pos]
+    linarith [Real.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]

Carleson/Theorem1_1/Carleson_on_the_real_line.lean

@@ -430,14 +430,14 @@ instance h6 : IsCZKernel 4 K where
     intro x y
     rw [Complex.norm_eq_abs, Real.vol, MeasureTheory.measureReal_def, Real.dist_eq, Real.volume_ball, ENNReal.toReal_ofReal (by linarith [abs_nonneg (x-y)])]
     calc Complex.abs (K x y)
-    _ ≤ 2 ^ (4 : ℝ) / (2 * |x - y|) := by apply Hilbert_kernel_bound
+    _ ≤ 2 ^ (2 : ℝ) / (2 * |x - y|) := by apply Hilbert_kernel_bound
     _ ≤ 2 ^ (4 : ℝ) ^ 3 / (2 * |x - y|) := by gcongr <;> norm_num
   /- uses Hilbert_kernel_regularity -/
   norm_sub_le := by
     intro x y y' h
     rw [Real.dist_eq, Real.dist_eq] at *
     calc ‖K x y - K x y'‖
-    _ ≤ 2 ^ 10 * (1 / |x - y|) * (|y - y'| / |x - y|) := by
+    _ ≤ 2 ^ 8 * (1 / |x - y|) * (|y - y'| / |x - y|) := by
       apply Hilbert_kernel_regularity
       linarith [abs_nonneg (x-y)]
     _ ≤ (|y - y'| / |x - y|) ^ (4 : ℝ)⁻¹ * (2 ^ (4 : ℝ) ^ 3 / Real.vol x y) := by

Carleson/Theorem1_1/ClassicalCarleson.lean

@@ -53,16 +53,7 @@ theorem classical_carleson {f : ℝ → ℂ}
   _ ≤ ε' + (ε / 4) + (ε / 4) := by
     gcongr
     . exact hf₀ x
-    . by_cases h : x = 2 * Real.pi
-      . rw [h, ←zero_add (2 * Real.pi), periodic_f₀, partialFourierSum_periodic]
-        apply hN₀ N NgtN₀ 0
-        simp [Real.pi_pos]
-      . have : x ∈ Set.Ico 0 (2 * Real.pi) := by
-          simp
-          simp at hx
-          use hx.1.1
-          apply lt_of_le_of_ne hx.1.2 h
-        convert hN₀ N NgtN₀ x this
+    . exact hN₀ N NgtN₀ x hx.1
     . have := hE x hx N
       rw [hdef, partialFourierSum_sub (contDiff_f₀.continuous.intervalIntegrable 0 (2 * Real.pi)) (unicontf.continuous.intervalIntegrable 0 (2 * Real.pi))] at this
       apply le_trans this
@@ -72,5 +63,5 @@ theorem classical_carleson {f : ℝ → ℂ}
     rw [ε'def, div_div]
     apply div_le_div_of_nonneg_left εpos.le (by norm_num)
     rw [← div_le_iff' (by norm_num)]
-    apply le_trans' (lt_C_control_approximation_effect εpos).le (by norm_num)
+    apply le_trans' (lt_C_control_approximation_effect εpos).le (by linarith [Real.two_le_pi])
   _ ≤ ε := by linarith

Carleson/Theorem1_1/Control_Approximation_Effect.lean

@@ -302,11 +302,11 @@ lemma le_CarlesonOperatorReal' {f : ℝ → ℂ} (hf : IntervalIntegrable f Meas
             apply Measurable.of_uncurry_left
             exact Hilbert_kernel_measurable
             measurability
-          have boundedness₁ {y : ℝ} (h : r ≤ dist x y) : ‖(I * (-↑n * ↑x)).exp * K x y * (I * ↑n * ↑y).exp‖ ≤ (2 ^ (4 : ℝ) / (2 * r)) := by
+          have boundedness₁ {y : ℝ} (h : r ≤ dist x y) : ‖(I * (-↑n * ↑x)).exp * K x y * (I * ↑n * ↑y).exp‖ ≤ (2 ^ (2 : ℝ) / (2 * r)) := by
             calc ‖(I * (-↑n * ↑x)).exp * K x y * (I * ↑n * ↑y).exp‖
               _ = ‖(I * (-↑n * ↑x)).exp‖ * ‖K x y‖ * ‖(I * ↑n * ↑y).exp‖ := by
                 rw [norm_mul, norm_mul]
-              _ ≤ 1 * (2 ^ (4 : ℝ) / (2 * |x - y|)) * 1 := by
+              _ ≤ 1 * (2 ^ (2 : ℝ) / (2 * |x - y|)) * 1 := by
                 gcongr
                 . rw [norm_eq_abs, mul_comm]
                   norm_cast
@@ -315,7 +315,7 @@ lemma le_CarlesonOperatorReal' {f : ℝ → ℂ} (hf : IntervalIntegrable f Meas
                 . rw [norm_eq_abs, mul_assoc, mul_comm]
                   norm_cast
                   rw [abs_exp_ofReal_mul_I]
-              _ ≤ (2 ^ (4 : ℝ) / (2 * r)) := by
+              _ ≤ (2 ^ (2 : ℝ) / (2 * r)) := by
                 rw [one_mul, mul_one, ← Real.dist_eq]
                 gcongr
           have integrable₁ := (integrable_annulus hx hf rpos.le rle1)
@@ -405,19 +405,19 @@ theorem rcarleson_exceptional_set_estimate_specific {δ : ℝ} (δpos : 0 < δ)
   ring_nf
 
 
-def C_control_approximation_effect (ε : ℝ) := (((C1_2 4 2 * (8 / (Real.pi * ε)) ^ (2 : ℝ)⁻¹)) + 8)
+def C_control_approximation_effect (ε : ℝ) := (C1_2 4 2 * (8 / (Real.pi * ε)) ^ (2 : ℝ)⁻¹) + Real.pi
 
-lemma lt_C_control_approximation_effect {ε : ℝ} (εpos : 0 < ε) : 8 < C_control_approximation_effect ε := by
+lemma lt_C_control_approximation_effect {ε : ℝ} (εpos : 0 < ε) : Real.pi < C_control_approximation_effect ε := by
   rw [C_control_approximation_effect]
   apply lt_add_of_pos_of_le _ (by rfl)
   apply mul_pos (C1_2_pos (by norm_num))
   apply Real.rpow_pos_of_pos
   apply div_pos (by norm_num)
   apply mul_pos Real.pi_pos εpos
 
-lemma C_control_approximation_effect_pos {ε : ℝ} (εpos : 0 < ε) : 0 < C_control_approximation_effect ε := lt_trans' (lt_C_control_approximation_effect εpos) (by norm_num)
+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_eq {ε : ℝ} {δ : ℝ} (ε_nonneg : 0 ≤ ε) : C_control_approximation_effect ε * δ = ((δ * C1_2 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ * (2 / ε) ^ (2 : ℝ)⁻¹) / Real.pi) + 8 * δ := by
+lemma C_control_approximation_effect_eq {ε : ℝ} {δ : ℝ} (ε_nonneg : 0 ≤ ε) : C_control_approximation_effect ε * δ = ((δ * C1_2 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ * (2 / ε) ^ (2 : ℝ)⁻¹) / Real.pi) + Real.pi * δ := 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]
   congr 2
@@ -509,7 +509,7 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real
         rfl
         intro _
         norm_num
-  have le_operator_add : ∀ x ∈ E, ENNReal.ofReal ((ε' - 8 * δ) * (2 * Real.pi)) ≤ T' f x + T' ((starRingEnd ℂ) ∘ f) x := by
+  have le_operator_add : ∀ x ∈ E, ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) ≤ T' f x + T' ((starRingEnd ℂ) ∘ f) x := by
     have h_intervalIntegrable' : IntervalIntegrable h MeasureTheory.volume 0 (2 * Real.pi) := by
       apply h_intervalIntegrable.mono_set
       rw [Set.uIcc_of_le (by linarith [Real.pi_pos]), Set.uIcc_of_le (by linarith [Real.pi_pos])]
@@ -520,9 +520,9 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real
     --set S := Set.Ioo (x - Real.pi) (x + Real.pi) with Sdef
     obtain ⟨xIcc, N, hN⟩ := hx
     rw [partialFourierSum_eq_conv_dirichletKernel' h_intervalIntegrable'] at hN
-    have : ENNReal.ofReal (8 * δ * (2 * Real.pi)) ≠ ⊤ := ENNReal.ofReal_ne_top
+    have : ENNReal.ofReal (Real.pi * δ * (2 * Real.pi)) ≠ ⊤ := ENNReal.ofReal_ne_top
     rw [← (ENNReal.add_le_add_iff_right this)]
-    calc ENNReal.ofReal ((ε' - 8 * δ) * (2 * Real.pi)) + ENNReal.ofReal (8 * δ * (2 * Real.pi))
+    calc ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) + ENNReal.ofReal (Real.pi * δ * (2 * Real.pi))
       _ = ENNReal.ofReal ((2 * Real.pi) * ε') := by
         rw [← ENNReal.ofReal_add]
         . congr
@@ -538,8 +538,7 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real
             apply Real.rpow_nonneg
             linarith [Real.pi_pos]
           . apply Real.rpow_nonneg (div_nonneg (by norm_num) hε.1.le)
-        . apply mul_nonneg _ Real.two_pi_pos.le
-          linarith
+        . apply mul_nonneg (mul_nonneg Real.pi_pos.le hδ.le) Real.two_pi_pos.le
       _ ≤ ENNReal.ofReal ((2 * Real.pi) * abs (1 / (2 * Real.pi) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), h y * dirichletKernel' N (x - y))) := by gcongr
       _ = ‖∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), h y * dirichletKernel' N (x - y)‖₊  := by
         rw [map_mul, map_div₀, ←mul_assoc]
@@ -587,7 +586,7 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real
         --apply abs.isAbsoluteValue.abv_add
         norm_cast
         apply nnnorm_add_le
-      _ ≤ (T' f x + T' ((starRingEnd ℂ) ∘ f) x) + ENNReal.ofReal (8 * δ * (2 * Real.pi)) := by
+      _ ≤ (T' f x + T' ((starRingEnd ℂ) ∘ f) x) + ENNReal.ofReal (Real.pi * δ * (2 * Real.pi)) := by
         --Estimate the two parts
         gcongr
         . --first part
@@ -669,7 +668,7 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real
           apply NNReal.le_toNNReal_of_coe_le
           rw [coe_nnnorm]
           calc ‖∫ (y : ℝ) in (x - Real.pi)..(x + Real.pi), h y * (min |x - y| 1) * dirichletKernel' N (x - y)‖
-            _ ≤ (δ * 8) * |(x + Real.pi) - (x - Real.pi)| := by
+            _ ≤ (δ * Real.pi) * |(x + Real.pi) - (x - Real.pi)| := by
               apply intervalIntegral.norm_integral_le_of_norm_le_const
               intro y hy
               rw [Set.uIoc_of_le (by linarith)] at hy
@@ -702,13 +701,13 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real
                     norm_cast
                     rw [abs_exp_ofReal_mul_I, one_div]
                 _ = 2 * (min |z| 1 / ‖1 - exp (I * z)‖) := by ring
-                _ ≤ 2 * 4 := by
-                  gcongr
+                _ ≤ 2 * (Real.pi / 2) := by
+                  gcongr 2 * ?_
+                  --. apply min_le_right
                   . by_cases h : (1 - exp (I * z)) = 0
-                    . rw [h]
-                      simp
-                    simp
-                    rw [div_le_iff', ←div_le_iff, ←norm_eq_abs]
+                    . rw [h, norm_zero, div_zero]
+                      linarith [Real.pi_pos]
+                    rw [div_le_iff', ←div_le_iff, div_div_eq_mul_div, mul_div_assoc, mul_comm]
                     apply lower_secant_bound'
                     . apply min_le_left
                     . have : |z| ≤ Real.pi := by
@@ -717,10 +716,10 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real
                         constructor <;> linarith [hy.1, hy.2]
                       rw [min_def]
                       split_ifs <;> linarith
-                    . norm_num
-                    . rwa [←norm_eq_abs, norm_pos_iff]
-                _ = 8 := by norm_num
-            _ = 8 * δ * (2 * Real.pi) := by
+                    . linarith [Real.pi_pos]
+                    . rwa [norm_pos_iff]
+                _ = Real.pi := by ring
+            _ = Real.pi * δ * (2 * Real.pi) := by
               simp
               rw [←two_mul, _root_.abs_of_nonneg Real.two_pi_pos.le]
               ring
@@ -735,9 +734,9 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real
       _ < ⊤ := ENNReal.ofReal_lt_top
   obtain ⟨E', E'subset, measurableSetE', E'measure, h⟩ := ENNReal.le_on_subset MeasureTheory.volume measurableSetE (CarlesonOperatorReal'_measurable f_measurable) (CarlesonOperatorReal'_measurable (Measurable.comp continuous_star.measurable f_measurable)) le_operator_add
   have E'volume : MeasureTheory.volume E' < ⊤ := lt_of_le_of_lt (MeasureTheory.measure_mono E'subset) Evolume
-  have : ENNReal.ofReal (Real.pi * (ε' - 8 * δ)) * MeasureTheory.volume E' ≤ ENNReal.ofReal (δ * C1_2 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹) * (MeasureTheory.volume E') ^ (2 : ℝ)⁻¹ := by
-    calc ENNReal.ofReal (Real.pi * (ε' - 8 * δ)) * MeasureTheory.volume E'
-    _ = ENNReal.ofReal ((ε' - 8 * δ) * (2 * Real.pi)) / 2 * MeasureTheory.volume E' := by
+  have : ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * MeasureTheory.volume E' ≤ ENNReal.ofReal (δ * C1_2 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹) * (MeasureTheory.volume E') ^ (2 : ℝ)⁻¹ := by
+    calc ENNReal.ofReal (Real.pi * (ε' - Real.pi * δ)) * MeasureTheory.volume E'
+    _ = ENNReal.ofReal ((ε' - Real.pi * δ) * (2 * Real.pi)) / 2 * MeasureTheory.volume E' := by
       congr
       rw [← ENNReal.ofReal_ofNat, ← ENNReal.ofReal_div_of_pos (by norm_num)]
       ring_nf
@@ -760,7 +759,7 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real
     apply mul_pos hδ (by rw [C1_2]; norm_num)
     apply Real.rpow_pos_of_pos
     linarith [Real.two_pi_pos]
-  have ε'_δ_expression_pos : 0 < Real.pi * (ε' - 8 * δ) := by
+  have ε'_δ_expression_pos : 0 < Real.pi * (ε' - Real.pi * δ) := by
     rw [ε'def, C_control_approximation_effect_eq hε.1.le, add_sub_cancel_right, mul_div_cancel₀ _ Real.pi_pos.ne.symm]
     apply mul_pos δ_mul_const_pos
     apply Real.rpow_pos_of_pos
@@ -775,7 +774,7 @@ lemma control_approximation_effect' {ε : ℝ} (hε : 0 < ε ∧ ε ≤ 2 * Real
       conv => lhs; rw [←Real.rpow_one (MeasureTheory.volume.real E')]
       congr
       norm_num
-    _ ≤ 2 * (δ * C1_2 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ / (Real.pi * (ε' - 8 * δ))) ^ (2 : ℝ) := by
+    _ ≤ 2 * (δ * C1_2 4 2 * (4 * Real.pi) ^ (2 : ℝ)⁻¹ / (Real.pi * (ε' - Real.pi * δ))) ^ (2 : ℝ) := by
       gcongr
       rw [Real.rpow_mul MeasureTheory.measureReal_nonneg]
       gcongr