chore(Analysis/Fourier): rename theorems (#31687)

Author: mcdoll

Mathlib/Analysis/Distribution/FourierSchwartz.lean

@@ -37,21 +37,21 @@ Schwartz space. -/
 def fourierTransformCLM : 𝓢(V, E) →L[𝕜] 𝓢(V, E) := by
   refine mkCLM ((𝓕 : (V → E) → (V → E)) ·) ?_ ?_ ?_ ?_
   · intro f g x
-    simp only [fourierIntegral_eq, add_apply, smul_add]
+    simp only [fourier_eq, add_apply, smul_add]
     rw [integral_add]
     · exact (fourierIntegral_convergent_iff _).2 f.integrable
     · exact (fourierIntegral_convergent_iff _).2 g.integrable
   · intro c f x
-    simp only [fourierIntegral_eq, smul_apply, smul_comm _ c, integral_smul, RingHom.id_apply]
+    simp only [fourier_eq, smul_apply, smul_comm _ c, integral_smul, RingHom.id_apply]
   · intro f
-    exact Real.contDiff_fourierIntegral (fun n _ ↦ integrable_pow_mul volume f n)
+    exact Real.contDiff_fourier (fun n _ ↦ integrable_pow_mul volume f n)
   · rintro ⟨k, n⟩
     refine ⟨Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1),
        (2 * π) ^ n * (2 * ↑n + 2) ^ k * (Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card
          * 2 ^ integrablePower (volume : Measure V) *
          (∫ (x : V), (1 + ‖x‖) ^ (- (integrablePower (volume : Measure V) : ℝ))) * 2,
        ⟨by positivity, fun f x ↦ ?_⟩⟩
-    apply (pow_mul_norm_iteratedFDeriv_fourierIntegral_le (f.smooth ⊤)
+    apply (pow_mul_norm_iteratedFDeriv_fourier_le (f.smooth ⊤)
       (fun k n _hk _hn ↦ integrable_pow_mul_iteratedFDeriv _ f k n) le_top le_top x).trans
     simp only [mul_assoc]
     gcongr
@@ -82,7 +82,7 @@ def fourierTransformCLM : 𝓢(V, E) →L[𝕜] 𝓢(V, E) := by
     _ = _ := by simp [mul_assoc]
 
 instance instFourierTransform : FourierTransform 𝓢(V, E) 𝓢(V, E) where
-  fourierTransform f := fourierTransformCLM ℂ f
+  fourier f := fourierTransformCLM ℂ f
 
 lemma fourier_coe (f : 𝓢(V, E)) : 𝓕 f = 𝓕 (f : V → E) := rfl
 
@@ -95,13 +95,13 @@ theorem fourierTransformCLM_apply (f : 𝓢(V, E)) :
     fourierTransformCLM 𝕜 f = 𝓕 f := rfl
 
 instance instFourierTransformInv : FourierTransformInv 𝓢(V, E) 𝓢(V, E) where
-  fourierTransformInv := (compCLMOfContinuousLinearEquiv ℂ (LinearIsometryEquiv.neg ℝ (E := V)))
+  fourierInv := (compCLMOfContinuousLinearEquiv ℂ (LinearIsometryEquiv.neg ℝ (E := V)))
       ∘L (fourierTransformCLM ℂ)
 
 lemma fourierInv_coe (f : 𝓢(V, E)) :
     𝓕⁻ f = 𝓕⁻ (f : V → E) := by
   ext x
-  exact (fourierIntegralInv_eq_fourierIntegral_neg f x).symm
+  exact (fourierInv_eq_fourier_neg f x).symm
 
 instance instFourierInvModule : FourierInvModule 𝕜 𝓢(V, E) 𝓢(V, E) where
   fourierInv_add := ContinuousLinearMap.map_add _
@@ -111,23 +111,24 @@ instance instFourierInvModule : FourierInvModule 𝕜 𝓢(V, E) 𝓢(V, E) wher
 variable [CompleteSpace E]
 
 instance instFourierPair : FourierPair 𝓢(V, E) 𝓢(V, E) where
-  inv_fourier := by
+  fourierInv_fourier_eq := by
     intro f
     ext x
-    rw [fourierInv_coe, fourier_coe, f.continuous.fourier_inversion f.integrable (𝓕 f).integrable]
+    rw [fourierInv_coe, fourier_coe, f.continuous.fourierInv_fourier_eq f.integrable
+      (𝓕 f).integrable]
 
 instance instFourierInvPair : FourierInvPair 𝓢(V, E) 𝓢(V, E) where
-  fourier_inv := by
+  fourier_fourierInv_eq := by
     intro f
     ext x
-    rw [fourier_coe, fourierInv_coe, f.continuous.fourier_inversion_inv f.integrable
+    rw [fourier_coe, fourierInv_coe, f.continuous.fourier_fourierInv_eq f.integrable
       (𝓕 f).integrable]
 
 @[deprecated (since := "2025-11-13")]
-alias fourier_inversion := FourierTransform.inv_fourier
+alias fourier_inversion := FourierTransform.fourierInv_fourier_eq
 
 @[deprecated (since := "2025-11-13")]
-alias fourier_inversion_inv := FourierTransform.fourier_inv
+alias fourier_inversion_inv := FourierTransform.fourier_fourierInv_eq
 
 /-- The Fourier transform on a real inner product space, as a continuous linear equiv on the
 Schwartz space. -/
@@ -154,22 +155,28 @@ variable [CompleteSpace E] [CompleteSpace F]
 
 /-- The Fourier transform satisfies `∫ 𝓕 f * g = ∫ f * 𝓕 g`, i.e., it is self-adjoint.
 Version where the multiplication is replaced by a general bilinear form `M`. -/
-theorem integral_bilin_fourierIntegral_eq (f : 𝓢(V, E)) (g : 𝓢(V, F)) (M : E →L[ℂ] F →L[ℂ] G) :
+theorem integral_bilin_fourier_eq (f : 𝓢(V, E)) (g : 𝓢(V, F)) (M : E →L[ℂ] F →L[ℂ] G) :
     ∫ ξ, M (𝓕 f ξ) (g ξ) = ∫ x, M (f x) (𝓕 g x) := by
   simpa using VectorFourier.integral_bilin_fourierIntegral_eq_flip M (L := (innerₗ V))
     continuous_fourierChar continuous_inner f.integrable g.integrable
 
-theorem integral_sesq_fourierIntegral_eq (f : 𝓢(V, E)) (g : 𝓢(V, F)) (M : E →L⋆[ℂ] F →L[ℂ] G) :
+@[deprecated (since := "2025-11-16")]
+alias integral_bilin_fourierIntegral_eq := integral_bilin_fourier_eq
+
+theorem integral_sesq_fourier_eq (f : 𝓢(V, E)) (g : 𝓢(V, F)) (M : E →L⋆[ℂ] F →L[ℂ] G) :
     ∫ ξ, M (𝓕 f ξ) (g ξ) = ∫ x, M (f x) (𝓕⁻ g x) := by
   simpa [fourierInv_coe] using VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip M
     (L := (innerₗ V)) continuous_fourierChar continuous_inner f.integrable g.integrable
 
+@[deprecated (since := "2025-11-16")]
+alias integral_sesq_fourierIntegral_eq := integral_sesq_fourier_eq
+
 /-- Plancherel's theorem for Schwartz functions.
 
 Version where the multiplication is replaced by a general bilinear form `M`. -/
 theorem integral_sesq_fourier_fourier (f : 𝓢(V, E)) (g : 𝓢(V, F)) (M : E →L⋆[ℂ] F →L[ℂ] G) :
     ∫ ξ, M (𝓕 f ξ) (𝓕 g ξ) = ∫ x, M (f x) (g x) := by
-  simpa using integral_sesq_fourierIntegral_eq f (𝓕 g) M
+  simpa using integral_sesq_fourier_eq f (𝓕 g) M
 
 end fubini
 

Mathlib/Analysis/Fourier/FourierTransform.lean

@@ -414,78 +414,117 @@ open scoped RealInnerProductSpace
 
 variable [FiniteDimensional ℝ V]
 
-instance FourierTransform : FourierTransform (V → E) (V → E) where
-  fourierTransform f := VectorFourier.fourierIntegral 𝐞 volume (innerₗ V) f
+instance instFourierTransform : FourierTransform (V → E) (V → E) where
+  fourier f := VectorFourier.fourierIntegral 𝐞 volume (innerₗ V) f
 
-instance FourierTransformInv : FourierTransformInv (V → E) (V → E) where
-  fourierTransformInv f w := VectorFourier.fourierIntegral 𝐞 volume (-innerₗ V) f w
+instance instFourierTransformInv : FourierTransformInv (V → E) (V → E) where
+  fourierInv f w := VectorFourier.fourierIntegral 𝐞 volume (-innerₗ V) f w
 
 @[deprecated (since := "2025-11-12")]
-alias fourierIntegral := FourierTransform.fourierTransform
+alias fourierIntegral := FourierTransform.fourier
 
 @[deprecated (since := "2025-11-12")]
-alias fourierIntegralInv := FourierTransform.fourierTransformInv
+alias fourierIntegralInv := FourierTransform.fourierInv
 
-lemma fourierIntegral_eq (f : V → E) (w : V) :
+lemma fourier_eq (f : V → E) (w : V) :
     𝓕 f w = ∫ v, 𝐞 (-⟪v, w⟫) • f v := rfl
 
-lemma fourierIntegral_eq' (f : V → E) (w : V) :
+@[deprecated (since := "2025-11-16")]
+alias fourierIntegral_eq := fourier_eq
+
+lemma fourier_eq' (f : V → E) (w : V) :
     𝓕 f w = ∫ v, Complex.exp ((↑(-2 * π * ⟪v, w⟫) * Complex.I)) • f v := by
-  simp_rw [fourierIntegral_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul]
+  simp_rw [fourier_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul]
+
+@[deprecated (since := "2025-11-16")]
+alias fourierIntegral_eq' := fourier_eq'
 
-lemma fourierIntegralInv_eq (f : V → E) (w : V) :
+lemma fourierInv_eq (f : V → E) (w : V) :
     𝓕⁻ f w = ∫ v, 𝐞 ⟪v, w⟫ • f v := by
-  simp [FourierTransformInv.fourierTransformInv, VectorFourier.fourierIntegral]
+  simp [FourierTransformInv.fourierInv, VectorFourier.fourierIntegral]
 
-lemma fourierIntegralInv_eq' (f : V → E) (w : V) :
+@[deprecated (since := "2025-11-16")]
+alias fourierIntegralInv_eq := fourierInv_eq
+
+lemma fourierInv_eq' (f : V → E) (w : V) :
     𝓕⁻ f w = ∫ v, Complex.exp ((↑(2 * π * ⟪v, w⟫) * Complex.I)) • f v := by
-  simp_rw [fourierIntegralInv_eq, Circle.smul_def, Real.fourierChar_apply]
+  simp_rw [fourierInv_eq, Circle.smul_def, Real.fourierChar_apply]
+
+@[deprecated (since := "2025-11-16")]
+alias fourierIntegralInv_eq' := fourierInv_eq'
 
-lemma fourierIntegral_comp_linearIsometry (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) :
+lemma fourier_comp_linearIsometry (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) :
     𝓕 (f ∘ A) w = (𝓕 f) (A w) := by
-  simp only [fourierIntegral_eq, ← A.inner_map_map, Function.comp_apply,
+  simp only [fourier_eq, ← A.inner_map_map, Function.comp_apply,
     ← MeasurePreserving.integral_comp A.measurePreserving A.toHomeomorph.measurableEmbedding]
 
-lemma fourierIntegralInv_eq_fourierIntegral_neg (f : V → E) (w : V) :
+@[deprecated (since := "2025-11-16")]
+alias fourierIntegral_comp_linearIsometry := fourier_comp_linearIsometry
+
+lemma fourierInv_eq_fourier_neg (f : V → E) (w : V) :
     𝓕⁻ f w = 𝓕 f (-w) := by
-  simp [fourierIntegral_eq, fourierIntegralInv_eq]
+  simp [fourier_eq, fourierInv_eq]
+
+@[deprecated (since := "2025-11-16")]
+alias fourierIntegralInv_eq_fourierIntegral_neg := fourierInv_eq_fourier_neg
 
-lemma fourierIntegralInv_eq_fourierIntegral_comp_neg (f : V → E) :
+lemma fourierInv_eq_fourier_comp_neg (f : V → E) :
     𝓕⁻ f = 𝓕 (fun x ↦ f (-x)) := by
   ext y
-  rw [fourierIntegralInv_eq_fourierIntegral_neg]
+  rw [fourierInv_eq_fourier_neg]
   change 𝓕 f (LinearIsometryEquiv.neg ℝ y) = 𝓕 (f ∘ LinearIsometryEquiv.neg ℝ) y
-  exact (fourierIntegral_comp_linearIsometry _ _ _).symm
+  exact (fourier_comp_linearIsometry _ _ _).symm
+
+@[deprecated (since := "2025-11-16")]
+alias fourierIntegralInv_eq_fourierIntegral_comp_neg := fourierInv_eq_fourier_comp_neg
 
-lemma fourierIntegralInv_comm (f : V → E) :
+lemma fourierInv_comm (f : V → E) :
     𝓕 (𝓕⁻ f) = 𝓕⁻ (𝓕 f) := by
-  conv_rhs => rw [fourierIntegralInv_eq_fourierIntegral_comp_neg]
-  simp_rw [← fourierIntegralInv_eq_fourierIntegral_neg]
+  conv_rhs => rw [fourierInv_eq_fourier_comp_neg]
+  simp_rw [← fourierInv_eq_fourier_neg]
 
-lemma fourierIntegralInv_comp_linearIsometry (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) :
+@[deprecated (since := "2025-11-16")]
+alias fourierIntegralInv_comm := fourierInv_comm
+
+lemma fourierInv_comp_linearIsometry (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W) :
     𝓕⁻ (f ∘ A) w = (𝓕⁻ f) (A w) := by
-  simp [fourierIntegralInv_eq_fourierIntegral_neg, fourierIntegral_comp_linearIsometry]
+  simp [fourierInv_eq_fourier_neg, fourier_comp_linearIsometry]
+
+@[deprecated (since := "2025-11-16")]
+alias fourierIntegralInv_comp_linearIsometry := fourierInv_comp_linearIsometry
 
-theorem fourierIntegral_real_eq (f : ℝ → E) (w : ℝ) :
+theorem fourier_real_eq (f : ℝ → E) (w : ℝ) :
     𝓕 f w = ∫ v : ℝ, 𝐞 (-(v * w)) • f v := by
   simp_rw [mul_comm _ w]
   rfl
 
-theorem fourierIntegral_real_eq_integral_exp_smul (f : ℝ → E) (w : ℝ) :
+@[deprecated (since := "2025-11-16")]
+alias fourierIntegral_real_eq := fourier_real_eq
+
+theorem fourier_real_eq_integral_exp_smul (f : ℝ → E) (w : ℝ) :
     𝓕 f w = ∫ v : ℝ, Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v := by
-  simp_rw [fourierIntegral_real_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul,
+  simp_rw [fourier_real_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul,
     mul_assoc]
 
-theorem fourierIntegral_continuousLinearMap_apply
+@[deprecated (since := "2025-11-16")]
+alias fourierIntegral_real_eq_integral_exp_smul := fourier_real_eq_integral_exp_smul
+
+theorem fourier_continuousLinearMap_apply
     {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
     {f : V → (F →L[ℝ] E)} {a : F} {v : V} (hf : Integrable f) :
     𝓕 f v a = 𝓕 (fun x ↦ f x a) v :=
   fourierIntegral_continuousLinearMap_apply' (L := innerSL ℝ) hf
 
-theorem fourierIntegral_continuousMultilinearMap_apply {ι : Type*} [Fintype ι]
+@[deprecated (since := "2025-11-16")]
+alias fourierIntegral_continuousLinearMap_apply := fourier_continuousLinearMap_apply
+
+theorem fourier_continuousMultilinearMap_apply {ι : Type*} [Fintype ι]
     {M : ι → Type*} [∀ i, NormedAddCommGroup (M i)] [∀ i, NormedSpace ℝ (M i)]
     {f : V → ContinuousMultilinearMap ℝ M E} {m : (i : ι) → M i} {v : V} (hf : Integrable f) :
     𝓕 f v m = 𝓕 (fun x ↦ f x m) v :=
   fourierIntegral_continuousMultilinearMap_apply' (L := innerSL ℝ) hf
 
+@[deprecated (since := "2025-11-16")]
+alias fourierIntegral_continuousMultilinearMap_apply := fourier_continuousMultilinearMap_apply
+
 end Real