Cleanup ProofData, extract iHolENorm and iLipENorm (includes task 401) (#493)

While cleaning up `ProofData.lean`, I decided to expand a bit and move
the definitions of `iHolENorm` and `iLipENorm` to separate files.
Biggest change is to make the tau parameter explicit, IMO this could not
be avoided.
There were some unexpected consequences of that because tau is an abbrev
and so is unfolded by any `simp` call.

I wasn't sure what ToMathlib folder these should go in, so I put them
under the main folder. I played around a bit with the assumptions to try
and minimize them.
Probably (quite) some work is required to bring these to Mathlib-worthy
completeness, generality and quality, it is expressly not my aim to
follow up on that (lacking the specific knowledge to determine
appropriate generality etc.).

But at least now the definitions and the results are completely
abstracted from the rest of Carleson.

Author: JasperMS

Carleson.lean

@@ -34,7 +34,9 @@ import Carleson.ForestOperator.PointwiseEstimate
 import Carleson.ForestOperator.QuantativeEstimate
 import Carleson.ForestOperator.RemainingTiles
 import Carleson.GridStructure
+import Carleson.HolderNorm
 import Carleson.HolderVanDerCorput
+import Carleson.LipschitzNorm
 import Carleson.MetricCarleson.Basic
 import Carleson.MetricCarleson.Linearized
 import Carleson.MetricCarleson.Main

Carleson/Antichain/TileCorrelation.lean

@@ -126,7 +126,7 @@ private lemma e625 {s₁ s₂ : ℤ} {x₁ x₂ y y' : X} (hy' : y ≠ y') (hs :
 
 /-- Second part of Lemma 6.2.1 (eq. 6.2.3). -/
 lemma correlation_kernel_bound {s₁ s₂ : ℤ} {x₁ x₂ : X} (hs : s₁ ≤ s₂) :
-    iHolENorm (correlation s₁ s₂ x₁ x₂) x₁ (2 * D ^ s₁) ≤
+    iHolENorm (correlation s₁ s₂ x₁ x₂) x₁ (2 * D ^ s₁) τ ≤
     C6_2_1 a / (volume (ball x₁ (D ^ s₁)) * volume (ball x₂ (D ^ s₂))) := by
   -- 6.2.4
   have hφ' (y : X) : ‖correlation s₁ s₂ x₁ x₂ y‖ₑ ≤
@@ -346,7 +346,7 @@ lemma I12_le' {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X → ℂ} (x1 : E
   gcongr
   · have hbdd := correlation_kernel_bound (a := a) (X := X) hle (x₁ := x1) (x₂ := x2)
     have hle : C2_0_5 a * volume (ball x1.1 (D ^ 𝔰 p')) *
-        iHolENorm (a := a) (correlation (𝔰 p') (𝔰 p) x1.1 x2.1) x1 (2 * D ^ 𝔰 p') ≤
+        iHolENorm (correlation (𝔰 p') (𝔰 p) x1.1 x2.1) x1 (2 * D ^ 𝔰 p') τ ≤
         C2_0_5 a * volume (ball x1.1 (D ^ 𝔰 p')) *
         (C6_2_1 a / (volume (ball x1.1 (D ^ 𝔰 p')) * volume (ball x2.1 (D ^ 𝔰 p)))) := by
       gcongr

Carleson/Defs.lean

@@ -112,13 +112,14 @@ class CompatibleFunctions (𝕜 : outParam Type*) (X : Type u) (A : outParam ℕ
   allBallsCoverBalls {x : X} {r : ℝ} :
     AllBallsCoverBalls (WithFunctionDistance x r) 2 A
 
+variable [hXA : DoublingMeasure X A]
+
 /-- The inhomogeneous Lipschitz norm on a ball. -/
-def iLipENorm {𝕜} [NormedField 𝕜] (ϕ : X → 𝕜) (x₀ : X) (R : ℝ) : ℝ≥0∞ :=
+def iLipENorm {𝕜 X : Type*} [NormedField 𝕜] [PseudoMetricSpace X]
+  (ϕ : X → 𝕜) (x₀ : X) (R : ℝ) : ℝ≥0∞ :=
   (⨆ x ∈ ball x₀ R, ‖ϕ x‖ₑ) +
   ENNReal.ofReal R * ⨆ (x ∈ ball x₀ R) (y ∈ ball x₀ R) (_ : x ≠ y), ‖ϕ x - ϕ y‖ₑ / edist x y
 
-variable [hXA : DoublingMeasure X A]
-
 variable (X) in
 /-- Θ is τ-cancellative. `τ` will usually be `1 / a` -/
 class IsCancellative (τ : ℝ) [CompatibleFunctions ℝ X A] : Prop where

Carleson/DoublingMeasure.lean

@@ -1,4 +1,5 @@
 import Carleson.Defs
+import Carleson.LipschitzNorm
 import Carleson.ToMathlib.Data.ENNReal
 
 open MeasureTheory Measure Metric Complex Set Bornology Function
@@ -104,12 +105,13 @@ lemma τ_pos : 0 < defaultτ a := inv_pos.mpr (cast_a_pos X)
 lemma τ_nonneg : 0 ≤ defaultτ a := (τ_pos X).le
 
 lemma τ_le_one : defaultτ a ≤ 1 := by
-
   rw [defaultτ, inv_le_one_iff₀]; right; norm_cast; linarith [four_le_a X]
 
 /-- `τ` as an element of `ℝ≥0`. -/
 def nnτ : ℝ≥0 := ⟨defaultτ a, τ_nonneg X⟩
 lemma nnτ_pos : 0 < nnτ X := τ_pos X
+@[simp]
+lemma nnτ_def : nnτ X = (defaultτ a).toNNReal := Real.toNNReal_of_nonneg (τ_nonneg X) |>.symm
 
 end KernelProofData
 
@@ -234,10 +236,6 @@ def cancelPt [CompatibleFunctions 𝕜 X A] : X :=
 lemma cancelPt_eq_zero [CompatibleFunctions 𝕜 X A] {f : Θ X} : f (cancelPt X) = 0 :=
   CompatibleFunctions.eq_zero (𝕜 := 𝕜) |>.choose_spec f
 
-/-- The `NNReal` version of the inhomogeneous Lipschitz norm on a ball, `iLipENorm`. -/
-def iLipNNNorm {𝕜} [NormedField 𝕜] (ϕ : X → 𝕜) (x₀ : X) (R : ℝ) : ℝ≥0 :=
-  (iLipENorm ϕ x₀ R).toNNReal
-
 variable [hXA : DoublingMeasure X A]
 
 lemma enorm_integral_exp_le [CompatibleFunctions ℝ X A] {τ : ℝ} [IsCancellative X τ]

Carleson/ForestOperator/LargeSeparation.lean

@@ -1764,7 +1764,7 @@ lemma le_C7_5_4 (ha : 4 ≤ a) :
 /-- Lemma 7.5.4. -/
 lemma holder_correlation_tree (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂)
     (hJ : J ∈ 𝓙₅ t u₁ u₂) (hf₁ : BoundedCompactSupport f₁) (hf₂ : BoundedCompactSupport f₂) :
-    iHolENorm (holderFunction t u₁ u₂ f₁ f₂ J) (c J) (16 * D ^ s J) ≤
+    iHolENorm (holderFunction t u₁ u₂ f₁ f₂ J) (c J) (16 * D ^ s J) τ ≤
     C7_5_4 a * P7_5_4 t u₁ u₂ f₁ f₂ J := by
   unfold iHolENorm
   calc
@@ -1934,7 +1934,7 @@ lemma cdtp_le_iHolENorm (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠
     (h2u : 𝓘 u₁ ≤ 𝓘 u₂) (hf₁ : BoundedCompactSupport f₁) (hf₂ : BoundedCompactSupport f₂) :
     ‖∫ x, adjointCarlesonSum (t u₁) f₁ x * conj (adjointCarlesonSum (t u₂ ∩ 𝔖₀ t u₁ u₂) f₂ x)‖ₑ ≤
     ∑ J ∈ 𝓙₅ t u₁ u₂, C2_0_5 a * volume (ball (c J) (8 * D ^ s J)) *
-      iHolENorm (holderFunction t u₁ u₂ f₁ f₂ J) (c J) (2 * (8 * D ^ s J)) *
+      iHolENorm (holderFunction t u₁ u₂ f₁ f₂ J) (c J) (2 * (8 * D ^ s J)) τ *
       (1 + edist_{c J, 8 * D ^ s J} (𝒬 u₂) (𝒬 u₁)) ^ (-(2 * a^2 + a^3 : ℝ)⁻¹) := by
   classical
   have rearr : ∀ J x, t.χ u₁ u₂ J x *

Carleson/HolderNorm.lean

@@ -0,0 +1,97 @@
+import Mathlib.Topology.MetricSpace.Holder
+
+open Set Metric Function ENNReal
+open scoped NNReal
+
+/-!
+# L^∞-normalized t-Hölder norm
+
+This file defines the L^∞-normalized t-Hölder norm, which probably in some form should end up in Mathlib.
+Lemmas about this norm that are proven in Carleson are collected here.
+
+TODO: Assess Mathlib-readiness, complete basic results, optimize imports.
+-/
+
+noncomputable section
+
+section Def
+
+variable {𝕜 X : Type*} [PseudoMetricSpace X] [NormedField 𝕜]
+
+/-- the L^∞-normalized t-Hölder norm. Defined in ℝ≥0∞ to avoid sup-related issues. -/
+def iHolENorm (φ : X → 𝕜) (x₀ : X) (R : ℝ) (t : ℝ) : ℝ≥0∞ :=
+  (⨆ (x ∈ ball x₀ R), ‖φ x‖ₑ) + (ENNReal.ofReal R) ^ t *
+    ⨆ (x ∈ ball x₀ R) (y ∈ ball x₀ R) (_ : x ≠ y), (‖φ x - φ y‖ₑ / (edist x y) ^ t)
+
+/-- The `NNReal` version of the L^∞-normalized t-Hölder norm, `iHolENorm`. -/
+def iHolNNNorm (φ : X → 𝕜) (x₀ : X) (R : ℝ) (t : ℝ) : ℝ≥0 :=
+  (iHolENorm φ x₀ R t).toNNReal
+
+end Def
+
+section iHolENorm
+
+variable {X 𝕜 : Type*} {x z : X} {R t : ℝ} {φ : X → 𝕜}
+variable [MetricSpace X] [NormedField 𝕜]
+
+lemma enorm_le_iHolENorm_of_mem (hx : x ∈ ball z R) : ‖φ x‖ₑ ≤ iHolENorm φ z R t := by
+  apply le_trans _ le_self_add
+  simp only [le_iSup_iff, iSup_le_iff]
+  tauto
+
+lemma HolderOnWith.of_iHolENorm_ne_top (ht : 0 ≤ t) (hφ : iHolENorm φ z R t ≠ ⊤) :
+    HolderOnWith (iHolNNNorm φ z R t / R.toNNReal ^ t) t.toNNReal φ (ball z R) := by
+  intro x hx y hy
+  have hR : 0 < R := by
+    simp only [mem_ball] at hx
+    apply dist_nonneg.trans_lt hx
+  rcases eq_or_ne x y with rfl | hne
+  · simp
+  have : (ENNReal.ofReal R) ^ t * (‖φ x - φ y‖ₑ / (edist x y) ^ t) ≤ iHolENorm φ z R t := calc
+    _ ≤ (ENNReal.ofReal R) ^ t *
+        ⨆ (x ∈ ball z R) (y ∈ ball z R) (_ : x ≠ y), (‖φ x - φ y‖ₑ / (edist x y) ^ t) := by
+      gcongr
+      simp only [ne_eq, le_iSup_iff, iSup_le_iff]
+      tauto
+    _ ≤ _ := le_add_self
+  rw [edist_eq_enorm_sub, ENNReal.coe_div (by simp [hR]), iHolNNNorm, coe_toNNReal hφ,
+    ← ENNReal.div_le_iff_le_mul (by simp [hne]) (by simp [edist_ne_top]),
+    ENNReal.le_div_iff_mul_le (by simp [hR]) (by simp)]
+  apply this.trans_eq'
+  rw [ENNReal.coe_rpow_of_ne_zero (by simp [hR]), Real.coe_toNNReal t ht, ENNReal.ofReal, mul_comm]
+
+lemma continuous_of_iHolENorm_ne_top (ht : 0 < t) (hφ : tsupport φ ⊆ ball z R)
+    (h'φ : iHolENorm φ z R t ≠ ∞) :
+    Continuous φ :=
+  HolderOnWith.of_iHolENorm_ne_top ht.le h'φ |>.continuousOn (by simp [ht])
+    |>.continuous_of_tsupport_subset isOpen_ball hφ
+
+lemma continuous_of_iHolENorm_ne_top' (ht : 0 < t) (hφ : support φ ⊆ ball z R)
+    (h'φ : iHolENorm φ z (2 * R) t ≠ ∞) :
+    Continuous φ := by
+  rcases le_or_gt R 0 with hR | hR
+  · have : support φ ⊆ ∅ := by rwa [ball_eq_empty.2 hR] at hφ
+    simp only [subset_empty_iff, support_eq_empty_iff] at this
+    simp only [this]
+    exact continuous_const
+  apply HolderOnWith.of_iHolENorm_ne_top ht.le h'φ |>.continuousOn (by simp [ht])
+    |>.continuous_of_tsupport_subset isOpen_ball
+  apply (closure_mono hφ).trans (closure_ball_subset_closedBall.trans ?_)
+  exact closedBall_subset_ball (by linarith)
+
+section iHolNNNorm
+
+lemma norm_le_iHolNNNorm_of_mem (hφ : iHolENorm φ z R t ≠ ⊤) (hx : x ∈ ball z R) :
+    ‖φ x‖ ≤ iHolNNNorm φ z R t :=
+  (ENNReal.toReal_le_toReal (by simp) hφ).2 (enorm_le_iHolENorm_of_mem hx)
+
+lemma norm_le_iHolNNNorm_of_subset (hφ : iHolENorm φ z R t ≠ ⊤) (h : support φ ⊆ ball z R) :
+    ‖φ x‖ ≤ iHolNNNorm φ z R t := by
+  by_cases hx : x ∈ ball z R
+  · apply norm_le_iHolNNNorm_of_mem hφ hx
+  · have : x ∉ support φ := fun a ↦ hx (h a)
+    simp [notMem_support.mp this]
+
+end iHolNNNorm
+
+end iHolENorm

Carleson/HolderVanDerCorput.lean

@@ -1,4 +1,5 @@
 import Carleson.TileStructure
+import Carleson.HolderNorm
 
 /-! This should roughly contain the contents of chapter 8. -/
 
@@ -236,17 +237,19 @@ lemma dist_holderApprox_le {z : X} {R t : ℝ} (hR : 0 < R) {C : ℝ≥0} (ht :
 
 lemma enorm_holderApprox_sub_le {z : X} {R t : ℝ} (hR : 0 < R) (ht : 0 < t) (h't : t ≤ 1)
     {ϕ : X → ℂ} (hϕ : support ϕ ⊆ ball z R) (x : X) :
-    ‖ϕ x - holderApprox R t ϕ x‖ₑ ≤ ENNReal.ofReal (t/2) ^ τ * iHolENorm ϕ z (2 * R) := by
-  rcases eq_or_ne (iHolENorm ϕ z (2 * R)) ∞ with h | h
+    ‖ϕ x - holderApprox R t ϕ x‖ₑ ≤ ENNReal.ofReal (t/2) ^ τ * iHolENorm ϕ z (2 * R) τ := by
+  rcases eq_or_ne (iHolENorm ϕ z (2 * R) τ) ∞ with h | h
   · apply le_top.trans_eq
     symm
+    simp only [defaultτ] at h
     simp [h, ENNReal.mul_eq_top, ht]
-  have : iHolENorm ϕ z (2 * R) = ENNReal.ofReal (iHolNNNorm ϕ z (2 * R)) := by
+  have : iHolENorm ϕ z (2 * R) τ = ENNReal.ofReal (iHolNNNorm ϕ z (2 * R) τ) := by
     simp only [iHolNNNorm, ENNReal.ofReal_coe_nnreal, ENNReal.coe_toNNReal h]
   rw [ENNReal.ofReal_rpow_of_pos (by linarith), this, ← ENNReal.ofReal_mul (by positivity),
     ← ofReal_norm_eq_enorm, ← dist_eq_norm]
   apply ENNReal.ofReal_le_ofReal
-  apply (dist_holderApprox_le hR ht h't hϕ (HolderOnWith.of_iHolENorm_ne_top h) x).trans_eq
+  apply dist_holderApprox_le hR ht h't hϕ
+    (by simpa [nnτ_def] using HolderOnWith.of_iHolENorm_ne_top (τ_nonneg X) h) x |>.trans_eq
   simp [field, NNReal.coe_div, hR.le]
 
 
@@ -471,14 +474,15 @@ lemma iLipENorm_holderApprox' {z : X} {R t : ℝ} (ht : 0 < t) (h't : t ≤ 1)
 lemma iLipENorm_holderApprox_le {z : X} {R t : ℝ} (ht : 0 < t) (h't : t ≤ 1)
     {ϕ : X → ℂ} (hϕ : support ϕ ⊆ ball z R) :
     iLipENorm (holderApprox R t ϕ) z (2 * R) ≤
-      2 ^ (4 * a) * (ENNReal.ofReal t) ^ (-1 - a : ℝ) * iHolENorm ϕ z (2 * R) := by
-  rcases eq_or_ne (iHolENorm ϕ z (2 * R)) ∞ with h'ϕ | h'ϕ
+      2 ^ (4 * a) * (ENNReal.ofReal t) ^ (-1 - a : ℝ) * iHolENorm ϕ z (2 * R) τ := by
+  rcases eq_or_ne (iHolENorm ϕ z (2 * R) τ) ∞ with h'ϕ | h'ϕ
   · apply le_top.trans_eq
     rw [eq_comm]
+    simp only [defaultτ] at h'ϕ
     simp [h'ϕ, ht]
   rw [← ENNReal.coe_toNNReal h'ϕ]
   apply iLipENorm_holderApprox' ht h't
-  · apply continuous_of_iHolENorm_ne_top' hϕ h'ϕ
+  · apply continuous_of_iHolENorm_ne_top' (τ_pos X) hϕ h'ϕ
   · exact hϕ
   · apply fun x ↦ norm_le_iHolNNNorm_of_subset h'ϕ (hϕ.trans ?_)
     intro y hy
@@ -495,16 +499,17 @@ def C2_0_5 (a : ℝ) : ℝ≥0 := 2 ^ (7 * a)
 theorem holder_van_der_corput {z : X} {R : ℝ} {ϕ : X → ℂ}
     (ϕ_supp : support ϕ ⊆ ball z R) {f g : Θ X} :
     ‖∫ x, exp (I * (f x - g x)) * ϕ x‖ₑ ≤
-    (C2_0_5 a : ℝ≥0∞) * volume (ball z R) * iHolENorm ϕ z (2 * R) *
+    (C2_0_5 a : ℝ≥0∞) * volume (ball z R) * iHolENorm ϕ z (2 * R) τ *
       (1 + edist_{z, R} f g) ^ (- (2 * a^2 + a^3 : ℝ)⁻¹) := by
   have : 4 ≤ a := four_le_a X
   have : (4 : ℝ) ≤ a := mod_cast four_le_a X
   rcases le_or_gt R 0 with hR | hR
   · simp [ball_eq_empty.2 hR, subset_empty_iff, support_eq_empty_iff] at ϕ_supp
     simp [ϕ_supp]
-  rcases eq_or_ne (iHolENorm ϕ z (2 * R)) ∞ with h2ϕ | h2ϕ
+  rcases eq_or_ne (iHolENorm ϕ z (2 * R) τ) ∞ with h2ϕ | h2ϕ
   · apply le_top.trans_eq
     symm
+    simp only [defaultτ] at h2ϕ
     have : (0 : ℝ) < 2 * a ^ 2 + a ^ 3 := by positivity
     simp [h2ϕ, C2_0_5, (measure_ball_pos volume z hR).ne', this, edist_ne_top]
   let t : ℝ := (1 + nndist_{z, R} f g) ^ (- (τ / (2 + a)))
@@ -514,7 +519,7 @@ theorem holder_van_der_corput {z : X} {R : ℝ} {ϕ : X → ℂ}
     · simp only [le_add_iff_nonneg_right,  NNReal.zero_le_coe]
     · simp only [defaultτ, Left.neg_nonpos_iff]
       positivity
-  have ϕ_cont : Continuous ϕ := continuous_of_iHolENorm_ne_top' ϕ_supp h2ϕ
+  have ϕ_cont : Continuous ϕ := continuous_of_iHolENorm_ne_top' (τ_pos X) ϕ_supp h2ϕ
   have ϕ_comp : HasCompactSupport ϕ := by
     apply HasCompactSupport.of_support_subset_isCompact (isCompact_closedBall z R)
     exact ϕ_supp.trans ball_subset_closedBall
@@ -546,14 +551,14 @@ theorem holder_van_der_corput {z : X} {R : ℝ} {ϕ : X → ℂ}
     · field_simp
       nlinarith
   have : ‖∫ x, exp (I * (f x - g x)) * ϕ' x‖ₑ ≤ 2 ^ (6 * a) * volume (ball z R)
-        * iHolENorm ϕ z (2 * R) * (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := calc
+        * iHolENorm ϕ z (2 * R) τ * (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := calc
       ‖∫ x, exp (I * (f x - g x)) * ϕ' x‖ₑ
     _ ≤ 2 ^ a * volume (ball z (2 * R))
       * iLipENorm ϕ' z (2 * R) * (1 + edist_{z, 2 * R} f g) ^ (- τ) := by
       simpa only [defaultA, Nat.cast_pow, Nat.cast_ofNat, t] using
         enorm_integral_exp_le (x := z) (r := 2 * R) (ϕ := ϕ') ϕ'_supp (f := f) (g := g)
     _ ≤ 2 ^ a * (2 ^ a * volume (ball z R))
-        * (2 ^ (4 * a) * (ENNReal.ofReal t) ^ (-1 - a : ℝ) * iHolENorm ϕ z (2 * R))
+        * (2 ^ (4 * a) * (ENNReal.ofReal t) ^ (-1 - a : ℝ) * iHolENorm ϕ z (2 * R) τ)
         * (1 + edist_{z, R} f g) ^ (- τ) := by
       gcongr 2 ^ a * ?_ * ?_ * ?_
       · exact iLipENorm_holderApprox_le t_pos t_one ϕ_supp
@@ -564,11 +569,11 @@ theorem holder_van_der_corput {z : X} {R : ℝ} {ϕ : X → ℂ}
         apply ENNReal.ofReal_le_ofReal
         apply CompatibleFunctions.cdist_mono
         apply ball_subset_ball (by linarith)
-    _ = 2 ^ (6 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) *
+    _ = 2 ^ (6 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) τ *
         ((ENNReal.ofReal t) ^ (-1 - a : ℝ) * (1 + edist_{z, R} f g) ^ (- τ)) := by
       rw [show 6 * a = 4 * a + a + a by ring, pow_add, pow_add]
       ring
-    _ ≤ 2 ^ (6 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) *
+    _ ≤ 2 ^ (6 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) τ *
         (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := by gcongr;
   /- Second step: control `‖∫ x, exp (I * (f x - g x)) * (ϕ x - ϕ' x)‖ₑ` using that `‖ϕ x - ϕ' x‖`
   is controlled pointwise, and vanishes outside of `B (z, 2R)`. -/
@@ -584,7 +589,7 @@ theorem holder_van_der_corput {z : X} {R : ℝ} {ϕ : X → ℂ}
     congr
     ring
   have : ‖∫ x, exp (I * (f x - g x)) * (ϕ x - ϕ' x)‖ₑ
-    ≤ 2 ^ (6 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) *
+    ≤ 2 ^ (6 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) τ *
         (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := calc
       ‖∫ x, exp (I * (f x - g x)) * (ϕ x - ϕ' x)‖ₑ
     _ = ‖∫ x in ball z (2 * R), exp (I * (f x - g x)) * (ϕ x - ϕ' x)‖ₑ := by
@@ -603,14 +608,14 @@ theorem holder_van_der_corput {z : X} {R : ℝ} {ϕ : X → ℂ}
       enorm_integral_le_lintegral_enorm _
     _ = ∫⁻ x in ball z (2 * R), ‖ϕ x - ϕ' x‖ₑ := by
       simp only [enorm_mul, ← ofReal_sub, enorm_exp_I_mul_ofReal, one_mul]
-    _ ≤ ∫⁻ x in ball z (2 * R), ENNReal.ofReal (t/2) ^ τ * iHolENorm ϕ z (2 * R) :=
+    _ ≤ ∫⁻ x in ball z (2 * R), ENNReal.ofReal (t/2) ^ τ * iHolENorm ϕ z (2 * R) τ :=
       lintegral_mono (fun x ↦ enorm_holderApprox_sub_le hR t_pos t_one ϕ_supp x)
-    _ = volume (ball z (2 * R)) * ENNReal.ofReal (t/2) ^ τ * iHolENorm ϕ z (2 * R) := by
+    _ = volume (ball z (2 * R)) * ENNReal.ofReal (t/2) ^ τ * iHolENorm ϕ z (2 * R) τ := by
       simp; ring
-    _ ≤ (2 ^ a * volume (ball z R)) * ENNReal.ofReal (t/2) ^ τ * iHolENorm ϕ z (2 * R) := by
+    _ ≤ (2 ^ a * volume (ball z R)) * ENNReal.ofReal (t/2) ^ τ * iHolENorm ϕ z (2 * R) τ := by
       gcongr
-    _ = 2 ^ a * volume (ball z R) * iHolENorm ϕ z (2 * R) * ENNReal.ofReal (t/2) ^ τ := by ring
-    _ ≤ 2 ^ (6 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) *
+    _ = 2 ^ a * volume (ball z R) * iHolENorm ϕ z (2 * R) τ * ENNReal.ofReal (t/2) ^ τ := by ring
+    _ ≤ 2 ^ (6 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) τ *
         (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := by
       gcongr
       · exact one_le_two
@@ -630,18 +635,18 @@ theorem holder_van_der_corput {z : X} {R : ℝ} {ϕ : X → ℂ}
       exact ϕ'_comp.mul_left
   _ ≤ ‖∫ x, exp (I * (f x - g x)) * (ϕ x - ϕ' x)‖ₑ + ‖∫ x, exp (I * (f x - g x)) * ϕ' x‖ₑ :=
     enorm_add_le _ _
-  _ ≤ 2 ^ (6 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) *
+  _ ≤ 2 ^ (6 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) τ *
         (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) +
-      2 ^ (6 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) *
+      2 ^ (6 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) τ *
         (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := by gcongr;
-  _ = 2 ^ (1 + 6 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) *
+  _ = 2 ^ (1 + 6 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) τ *
         (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := by rw [pow_add, pow_one]; ring
-  _ ≤ 2 ^ (7 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) *
+  _ ≤ 2 ^ (7 * a) * volume (ball z R) * iHolENorm ϕ z (2 * R) τ *
         (1 + edist_{z, R} f g) ^ (- τ ^ 2 / (2 + a)) := by
     gcongr
     · exact one_le_two
     · linarith
-  _ = (C2_0_5 a : ℝ≥0∞) * volume (ball z R) * iHolENorm ϕ z (2 * R) *
+  _ = (C2_0_5 a : ℝ≥0∞) * volume (ball z R) * iHolENorm ϕ z (2 * R) τ *
       (1 + edist_{z, R} f g) ^ (- (2 * a^2 + a^3 : ℝ)⁻¹) := by
     congr
     · simp only [C2_0_5]