Rename phi (03D5) to phi (03C6) (#515)

This PR replaces `ϕ` (U+03D5) with `φ` (U+03C6) throughout. The reason
is that `\phi` in VS Code yields the latter symbol.

This type of PR rots quickly, so it would be nice if it can be
incorporated soon-ish.

Author: JasperMS

Carleson/Classical/CarlesonOnTheRealLine.lean

@@ -391,21 +391,21 @@ open scoped NNReal
 
 instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) := by
   apply isCancellative_of_norm_integral_exp_le
-  intro x r ϕ r_pos hK hϕ f g
+  intro x r φ r_pos hK hφ f g
   rw [defaultτ, ← one_div, measureReal_def, Real.volume_ball,
     ENNReal.toReal_ofReal (by linarith [r_pos]), Real.ball_eq_Ioo, ← integral_Ioc_eq_integral_Ioo,
     ← intervalIntegral.integral_of_le (by linarith [r_pos]), dist_integer_linear_eq,
     max_eq_left r_pos.le]
-  calc ‖∫ (x : ℝ) in x - r..x + r, (Complex.I * (↑(f x) - ↑(g x))).exp * ϕ x‖
-    _ = ‖∫ (x : ℝ) in x - r..x + r, (Complex.I * ((↑f - ↑g) : ℤ) * x).exp * ϕ x‖ := by
+  calc ‖∫ (x : ℝ) in x - r..x + r, (Complex.I * (↑(f x) - ↑(g x))).exp * φ x‖
+    _ = ‖∫ (x : ℝ) in x - r..x + r, (Complex.I * ((↑f - ↑g) : ℤ) * x).exp * φ x‖ := by
       congr with x
       rw [mul_assoc]
       congr
       push_cast
       rw [_root_.sub_mul]
       norm_cast
-    _ ≤ 2 * π * ((x + r) - (x - r)) * (iLipNNNorm ϕ x r +
-          (iLipNNNorm ϕ x r / r.toNNReal : ℝ≥0) * ((x + r) - (x - r)) / 2) *
+    _ ≤ 2 * π * ((x + r) - (x - r)) * (iLipNNNorm φ x r +
+          (iLipNNNorm φ x r / r.toNNReal : ℝ≥0) * ((x + r) - (x - r)) / 2) *
       (1 + |((↑f - ↑g) : ℤ)| * ((x + r) - (x - r)))⁻¹ := by
       apply van_der_Corput (by linarith)
       · rw [Ioo_eq_ball]
@@ -414,15 +414,15 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) := by
       · intro y hy
         apply norm_le_iLipNNNorm_of_mem hK
         rwa [Real.ball_eq_Ioo]
-    _ = 2 * π * (2 * r) * (iLipNNNorm ϕ x r + r * (iLipNNNorm ϕ x r / r.toNNReal : ℝ≥0))
+    _ = 2 * π * (2 * r) * (iLipNNNorm φ x r + r * (iLipNNNorm φ x r / r.toNNReal : ℝ≥0))
           * (1 + 2 * r * |((↑f - ↑g) : ℤ)|)⁻¹ := by
       ring
-    _ = 2 * π * (2 * r) * (iLipNNNorm ϕ x r + iLipNNNorm ϕ x r)
+    _ = 2 * π * (2 * r) * (iLipNNNorm φ x r + iLipNNNorm φ x r)
           * (1 + 2 * r * |((↑f - ↑g) : ℤ)|)⁻¹ := by
       congr
       rw [NNReal.coe_div, Real.coe_toNNReal _ r_pos.le, mul_div_cancel₀ _ r_pos.ne']
-    _ = 4 * π * (2 * r) * iLipNNNorm ϕ x r * (1 + 2 * r * ↑|(↑f - ↑g : ℤ)|)⁻¹ := by ring
-    _ ≤ (2 ^ 4 : ℕ) * (2 * r) * iLipNNNorm ϕ x r *
+    _ = 4 * π * (2 * r) * iLipNNNorm φ x r * (1 + 2 * r * ↑|(↑f - ↑g : ℤ)|)⁻¹ := by ring
+    _ ≤ (2 ^ 4 : ℕ) * (2 * r) * iLipNNNorm φ x r *
       (1 + 2 * r * ↑|(↑f - ↑g : ℤ)|) ^ (- (1 / (4 : ℝ))) := by
       gcongr
       · norm_num

Carleson/Classical/VanDerCorput.lean

@@ -46,18 +46,18 @@ lemma intervalIntegrable_continuous_mul_lipschitzOnWith
     apply mem_image_of_mem
     exact Ioo_subset_Icc_self hx
 
-lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B K : ℝ≥0}
-    (h1 : LipschitzOnWith K ϕ (Ioo a b)) (h2 : ∀ x ∈ Ioo a b, ‖ϕ x‖ ≤ B) :
-    ‖∫ x in a..b, exp (I * n * x) * ϕ x‖ ≤
+lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {φ : ℝ → ℂ} {B K : ℝ≥0}
+    (h1 : LipschitzOnWith K φ (Ioo a b)) (h2 : ∀ x ∈ Ioo a b, ‖φ x‖ ≤ B) :
+    ‖∫ x in a..b, exp (I * n * x) * φ x‖ ≤
      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
   · rw [n_nonzero]
     simp only [Int.cast_zero, mul_zero, zero_mul, exp_zero, one_mul, abs_zero,
       add_zero, inv_one, mul_one]
-    calc ‖∫ x in a..b, ϕ x‖
-      _ = ‖∫ x in Set.Ioo a b, ϕ x‖ := by
+    calc ‖∫ x in a..b, φ x‖
+      _ = ‖∫ x in Set.Ioo a b, φ x‖ := by
         rw [intervalIntegral.integral_of_le, ← integral_Ioc_eq_integral_Ioo]
         linarith
       _ ≤ B * (volume (Set.Ioo a b)).toReal := by
@@ -72,14 +72,14 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
         · exact sub_nonneg_of_le hab
         · linarith [Real.two_le_pi]
         · exact (le_add_iff_nonneg_right ↑B).mpr hK
-  wlog n_pos : 0 < n generalizing n ϕ
+  wlog n_pos : 0 < n generalizing n φ
   · /-We could do calculations analogous to those below. Instead, we apply the positive
     case to the complex conjugate.-/
     push_neg at n_pos
-    calc ‖∫ x in a..b, cexp (I * ↑n * ↑x) * ϕ x‖
-      _ = ‖(starRingEnd ℂ) (∫ x in a..b, cexp (I * ↑n * ↑x) * ϕ x)‖ :=
+    calc ‖∫ x in a..b, cexp (I * ↑n * ↑x) * φ x‖
+      _ = ‖(starRingEnd ℂ) (∫ x in a..b, cexp (I * ↑n * ↑x) * φ x)‖ :=
         (RCLike.norm_conj _).symm
-      _ = ‖∫ x in a..b, cexp (I * ↑(-n) * ↑x) * ((starRingEnd ℂ) ∘ ϕ) x‖ := by
+      _ = ‖∫ x in a..b, cexp (I * ↑(-n) * ↑x) * ((starRingEnd ℂ) ∘ φ) x‖ := by
         rw [intervalIntegral.integral_of_le (by linarith), ← integral_conj,
           ← intervalIntegral.integral_of_le (by linarith)]
         congr
@@ -107,7 +107,7 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
       apply add_pos_of_pos_of_nonneg zero_lt_one
       apply mul_nonneg (by simp) (by linarith)
     calc _
-      _ = ‖∫ x in Set.Ioo a b, cexp (I * ↑n * ↑x) * ϕ x‖ := by
+      _ = ‖∫ x in Set.Ioo a b, cexp (I * ↑n * ↑x) * φ x‖ := by
         rw [intervalIntegral.integral_of_le, ← integral_Ioc_eq_integral_Ioo]
         linarith
       _ ≤ B * (volume (Set.Ioo a b)).toReal := by
@@ -137,30 +137,30 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
   push_neg at h
   have pi_div_n_pos : 0 < π / n := div_pos Real.pi_pos (Int.cast_pos.mpr n_pos)
   calc _
-    _ = ‖∫ x in a..b, (1 / 2 * exp (I * n * x) - 1 / 2 * exp (I * ↑n * (↑x + ↑π / ↑n))) * ϕ x‖ := by
+    _ = ‖∫ x in a..b, (1 / 2 * exp (I * n * x) - 1 / 2 * exp (I * ↑n * (↑x + ↑π / ↑n))) * φ x‖ := by
       congr
       ext x
       congr
       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 + ↑π / ↑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, exp (I * n * x) * ϕ x)
-                      - (∫ x in a..b, exp (I * n * (x + π / n)) * ϕ x)‖ := by
+    _ = 1 / 2 * ‖(∫ x in a..b, exp (I * n * x) * φ x)
+                      - (∫ x in a..b, exp (I * n * (x + π / n)) * φ x)‖ := by
       rw [norm_mul]
       congr
       · simp
       rw [← intervalIntegral.integral_sub]
       · exact intervalIntegrable_continuous_mul_lipschitzOnWith hab (by fun_prop) h1
       · exact intervalIntegrable_continuous_mul_lipschitzOnWith hab (by fun_prop) h1
-    _ = 1 / 2 * ‖  (∫ x in a..(a + π / n), exp (I * n * x) * ϕ x)
-                 + (∫ x in (a + π / n)..b, exp (I * n * x) * ϕ x)
-                 -((∫ x in a..(b - π / n), exp (I * n * (x + π / n)) * ϕ x)
-                 + (∫ x in (b - π / n)..b, exp (I * n * (x + π / n)) * ϕ x))‖ := by
+    _ = 1 / 2 * ‖  (∫ x in a..(a + π / n), exp (I * n * x) * φ x)
+                 + (∫ x in (a + π / n)..b, exp (I * n * x) * φ x)
+                 -((∫ x in a..(b - π / n), exp (I * n * (x + π / n)) * φ x)
+                 + (∫ x in (b - π / n)..b, exp (I * n * (x + π / n)) * φ x))‖ := by
       congr 3
       · rw [intervalIntegral.integral_add_adjacent_intervals]
         · exact intervalIntegrable_continuous_mul_lipschitzOnWith (by linarith) (by fun_prop)
@@ -172,47 +172,47 @@ lemma van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B
             (h1.mono (Ioo_subset_Ioo le_rfl (by linarith)))
         · exact intervalIntegrable_continuous_mul_lipschitzOnWith (by linarith) (by fun_prop)
             (h1.mono (Ioo_subset_Ioo (by linarith) le_rfl))
-    _ = 1 / 2 * ‖  (∫ x in a..(a + π / n), exp (I * n * x) * ϕ x)
-                 + (∫ x in (a + π / n)..b, exp (I * n * x) * ϕ x)
-                 -((∫ x in (a + π / n)..(b - π / n + π / n), exp (I * n * x) * ϕ (x - π / n))
-                 + (∫ x in (b - π / n)..b, exp (I * n * (x + π / n)) * ϕ x))‖ := by
+    _ = 1 / 2 * ‖  (∫ x in a..(a + π / n), exp (I * n * x) * φ x)
+                 + (∫ x in (a + π / n)..b, exp (I * n * x) * φ x)
+                 -((∫ x in (a + π / n)..(b - π / n + π / n), exp (I * n * x) * φ (x - π / n))
+                 + (∫ x in (b - π / n)..b, exp (I * n * (x + π / n)) * φ x))‖ := by
       congr 4
       rw [← intervalIntegral.integral_comp_add_right]
       simp
-    _ = 1 / 2 * ‖  (∫ x in a..(a + π / n), exp (I * n * x) * ϕ x)
-                 +((∫ x in (a + π / n)..b, exp (I * n * x) * ϕ x)
-                 - (∫ x in (a + π / n)..b, exp (I * n * x) * ϕ (x - π / n)))
-                 - (∫ x in (b - π / n)..b, exp (I * n * (x + π / n)) * ϕ x)‖ := by
+    _ = 1 / 2 * ‖  (∫ x in a..(a + π / n), exp (I * n * x) * φ x)
+                 +((∫ x in (a + π / n)..b, exp (I * n * x) * φ x)
+                 - (∫ x in (a + π / n)..b, exp (I * n * x) * φ (x - π / n)))
+                 - (∫ x in (b - π / n)..b, exp (I * n * (x + π / n)) * φ x)‖ := by
       congr 2
       rw [sub_add_cancel]
       ring
-    _ = 1 / 2 * ‖  (∫ x in a..(a + π / n), exp (I * n * x) * ϕ x)
-                 + (∫ x in (a + π / n)..b, exp (I * n * x) * (ϕ x - ϕ (x - π / n)))
-                 - (∫ x in (b - π / n)..b, exp (I * n * (x + π / n)) * ϕ x)‖ := by
+    _ = 1 / 2 * ‖  (∫ x in a..(a + π / n), exp (I * n * x) * φ x)
+                 + (∫ x in (a + π / n)..b, exp (I * n * x) * (φ x - φ (x - π / n)))
+                 - (∫ x in (b - π / n)..b, exp (I * n * (x + π / n)) * φ x)‖ := by
       congr 4
       rw [← intervalIntegral.integral_sub]
       · congr
         ext x
         ring
       · exact intervalIntegrable_continuous_mul_lipschitzOnWith (by linarith) (by fun_prop)
           (h1.mono (Ioo_subset_Ioo (by linarith) le_rfl))
-      · have : IntervalIntegrable (fun x ↦ cexp (I * ↑n * (x + π / n)) * ϕ x)
+      · have : IntervalIntegrable (fun x ↦ cexp (I * ↑n * (x + π / n)) * φ x)
             volume a (b - π / n) := intervalIntegrable_continuous_mul_lipschitzOnWith
           (by linarith) (by fun_prop) (h1.mono (Ioo_subset_Ioo le_rfl (by linarith)))
         simpa using this.comp_sub_right (π / n)
-    _ ≤ 1 / 2 * (  ‖(∫ x in a..(a + π / n), exp (I * n * x) * ϕ x)
-                 +  (∫ x in (a + π / n)..b, exp (I * n * x) * (ϕ x - ϕ (x - π / n)))‖
-                 + ‖∫ x in (b - π / n)..b, exp (I * n * (x + π / n)) * ϕ x‖) := by
+    _ ≤ 1 / 2 * (  ‖(∫ x in a..(a + π / n), exp (I * n * x) * φ x)
+                 +  (∫ x in (a + π / n)..b, exp (I * n * x) * (φ x - φ (x - π / n)))‖
+                 + ‖∫ x in (b - π / n)..b, exp (I * n * (x + π / n)) * φ x‖) := by
       gcongr
       exact norm_sub_le ..
-    _ ≤ 1 / 2 * (  ‖(∫ x in a..(a + π / n), exp (I * n * x) * ϕ x)‖
-                 + ‖(∫ x in (a + π / n)..b, exp (I * n * x) * (ϕ x - ϕ (x - π / n)))‖
-                 + ‖∫ x in (b - π / n)..b, exp (I * n * (x + π / n)) * ϕ x‖) := by
+    _ ≤ 1 / 2 * (  ‖(∫ x in a..(a + π / n), exp (I * n * x) * φ x)‖
+                 + ‖(∫ x in (a + π / n)..b, exp (I * n * x) * (φ x - φ (x - π / n)))‖
+                 + ‖∫ x in (b - π / n)..b, exp (I * n * (x + π / n)) * φ x‖) := by
       gcongr
       exact norm_add_le ..
-    _ = 1 / 2 * (  ‖∫ x in Ioo a (a + π / n), exp (I * n * x) * ϕ x‖
-                 + ‖∫ x in Ioo (a + π / n) b, exp (I * n * x) * (ϕ x - ϕ (x - π / n))‖
-                 + ‖∫ x in Ioo (b - π / n) b, exp (I * n * (x + π / n)) * ϕ x‖) := by
+    _ = 1 / 2 * (  ‖∫ x in Ioo a (a + π / n), exp (I * n * x) * φ x‖
+                 + ‖∫ x in Ioo (a + π / n) b, exp (I * n * x) * (φ x - φ (x - π / n))‖
+                 + ‖∫ x in Ioo (b - π / n) b, exp (I * n * (x + π / n)) * φ x‖) := by
       congr
       all_goals
         rw [intervalIntegral.integral_of_le, ← integral_Ioc_eq_integral_Ioo]

Carleson/Defs.lean

@@ -116,19 +116,19 @@ variable [hXA : DoublingMeasure X A]
 
 /-- The inhomogeneous Lipschitz norm on a ball. -/
 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
+  (φ : 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 (X) in
 /-- Θ is τ-cancellative. `τ` will usually be `1 / a` -/
 class IsCancellative (τ : ℝ) [CompatibleFunctions ℝ X A] : Prop where
   /- We register a definition with strong assumptions, which makes them easier to prove.
   However, `enorm_integral_exp_le` removes them for easier application. -/
-  enorm_integral_exp_le' {x : X} {r : ℝ} {ϕ : X → ℂ} (hr : 0 < r) (h1 : iLipENorm ϕ x r ≠ ∞)
-    (h2 : support ϕ ⊆ ball x r) {f g : Θ X} :
-    ‖∫ x, exp (I * (f x - g x)) * ϕ x‖ₑ ≤
-    (A : ℝ≥0∞) * volume (ball x r) * iLipENorm ϕ x r * (1 + edist_{x, r} f g) ^ (- τ)
+  enorm_integral_exp_le' {x : X} {r : ℝ} {φ : X → ℂ} (hr : 0 < r) (h1 : iLipENorm φ x r ≠ ∞)
+    (h2 : support φ ⊆ ball x r) {f g : Θ X} :
+    ‖∫ x, exp (I * (f x - g x)) * φ x‖ₑ ≤
+    (A : ℝ≥0∞) * volume (ball x r) * iLipENorm φ x r * (1 + edist_{x, r} f g) ^ (- τ)
 
 /-- The "volume function" `V`. Preferably use `vol` instead. -/
 protected def Real.vol {X : Type*} [PseudoMetricSpace X] [MeasureSpace X] (x y : X) : ℝ :=

Carleson/DoublingMeasure.lean

@@ -239,9 +239,9 @@ lemma cancelPt_eq_zero [CompatibleFunctions 𝕜 X A] {f : Θ X} : f (cancelPt X
 variable [hXA : DoublingMeasure X A]
 
 lemma enorm_integral_exp_le [CompatibleFunctions ℝ X A] {τ : ℝ} [IsCancellative X τ]
-    {x : X} {r : ℝ} {ϕ : X → ℂ} (h2 : support ϕ ⊆ ball x r) {f g : Θ X} :
-    ‖∫ x, exp (I * (f x - g x)) * ϕ x‖ₑ ≤
-    (A : ℝ≥0∞) * volume (ball x r) * iLipENorm ϕ x r * (1 + edist_{x, r} f g) ^ (- τ) := by
+    {x : X} {r : ℝ} {φ : X → ℂ} (h2 : support φ ⊆ ball x r) {f g : Θ X} :
+    ‖∫ x, exp (I * (f x - g x)) * φ x‖ₑ ≤
+    (A : ℝ≥0∞) * volume (ball x r) * iLipENorm φ x r * (1 + edist_{x, r} f g) ^ (- τ) := by
   rcases le_or_gt r 0 with hr | hr
   · simp only [ball_eq_empty.2 hr, subset_empty_iff, support_eq_empty_iff] at h2
     simp [h2]
@@ -251,26 +251,26 @@ lemma enorm_integral_exp_le [CompatibleFunctions ℝ X A] {τ : ℝ} [IsCancella
       simp at this
       apply eq_zero_of_isDoubling_zero
     simp [this]
-  rcases eq_or_ne (iLipENorm ϕ x r) ∞ with h1 | h1
+  rcases eq_or_ne (iLipENorm φ x r) ∞ with h1 | h1
   · apply le_top.trans_eq
     symm
     simp [h1, edist_ne_top, hA, (measure_ball_pos volume x hr).ne']
   exact IsCancellative.enorm_integral_exp_le' hr h1 h2
 
 /-- Constructor of `IsCancellative` in terms of real norms instead of extended reals. -/
 lemma isCancellative_of_norm_integral_exp_le (τ : ℝ) [CompatibleFunctions ℝ X A]
-    (h : ∀ {x : X} {r : ℝ} {ϕ : X → ℂ} (_hr : 0 < r) (_h1 : iLipENorm ϕ x r ≠ ∞)
-    (_h2 : support ϕ ⊆ ball x r) {f g : Θ X},
-      ‖∫ x in ball x r, exp (I * (f x - g x)) * ϕ x‖ ≤
-      A * volume.real (ball x r) * iLipNNNorm ϕ x r * (1 + dist_{x, r} f g) ^ (-τ)) :
+    (h : ∀ {x : X} {r : ℝ} {φ : X → ℂ} (_hr : 0 < r) (_h1 : iLipENorm φ x r ≠ ∞)
+    (_h2 : support φ ⊆ ball x r) {f g : Θ X},
+      ‖∫ x in ball x r, exp (I * (f x - g x)) * φ x‖ ≤
+      A * volume.real (ball x r) * iLipNNNorm φ x r * (1 + dist_{x, r} f g) ^ (-τ)) :
     IsCancellative X τ := by
   constructor
-  intro x r ϕ hr h1 h2 f g
-  convert ENNReal.ofReal_le_ofReal (h (x := x) (r := r) (ϕ := ϕ) hr h1 h2 (f := f) (g := g))
+  intro x r φ hr h1 h2 f g
+  convert ENNReal.ofReal_le_ofReal (h (x := x) (r := r) (φ := φ) hr h1 h2 (f := f) (g := g))
   · rw [ofReal_norm_eq_enorm]
     congr 1
     rw [setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)]
-    have : ϕ y = 0 := by
+    have : φ y = 0 := by
       apply notMem_support.1
       contrapose! hy
       exact h2 hy