refactor(Analysis/Fourier): use AddChar machinery in `FourierTransf…

…orm` (#11417)

The file `Analysis/Fourier/FourierTransform.lean` predates the general approach to additive characters elsewhere in the library; this merges the two (getting rid of the rather kludgy notation `e [x]` in the process).  I also rejigged some slow proofs, to make them compile slightly faster.

Mathlib/Analysis/Complex/Circle.lean

@@ -156,3 +156,9 @@ theorem expMapCircle_sub (x y : ℝ) : expMapCircle (x - y) = expMapCircle x / e
 theorem expMapCircle_neg (x : ℝ) : expMapCircle (-x) = (expMapCircle x)⁻¹ :=
   expMapCircleHom.map_neg x
 #align exp_map_circle_neg expMapCircle_neg
+
+@[simp]
+lemma norm_circle_smul {E : Type*} [SeminormedAddCommGroup E] [NormedSpace ℂ E]
+    (u : circle) (v : E) :
+    ‖u • v‖ = ‖v‖ := by
+  rw [Submonoid.smul_def, norm_smul, norm_eq_of_mem_sphere, one_mul]

Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

@@ -24,16 +24,12 @@ open Real Complex MeasureTheory Filter TopologicalSpace
 
 open scoped FourierTransform Topology
 
-lemma Real.hasDerivAt_fourierChar (x : ℝ) :
-    HasDerivAt (fun y : ℝ ↦ (fourierChar (Multiplicative.ofAdd y) : ℂ))
-      (2 * π * I * (fourierChar (Multiplicative.ofAdd x) : ℂ)) x := by
-  have h1 (y : ℝ) : (fourierChar (Multiplicative.ofAdd y) : ℂ) =
-      fourier 1 (y : UnitAddCircle) := by
+lemma Real.hasDerivAt_fourierChar (x : ℝ) : HasDerivAt (𝐞 · : ℝ → ℂ) (2 * π * I * 𝐞 x) x := by
+  have h1 (y : ℝ) : 𝐞 y = fourier 1 (y : UnitAddCircle) := by
     rw [fourierChar_apply, fourier_coe_apply]
     push_cast
     ring_nf
-  simpa only [h1, Int.cast_one, ofReal_one, div_one, mul_one]
-    using hasDerivAt_fourier 1 1 x
+  simpa only [h1, Int.cast_one, ofReal_one, div_one, mul_one] using hasDerivAt_fourier 1 1 x
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
 
@@ -48,28 +44,27 @@ def mul_L (v : V) : (W →L[ℝ] E) := -(2 * π * I) • (L v).smulRight (f v)
 
 /-- The `w`-derivative of the Fourier transform integrand. -/
 lemma hasFDerivAt_fourier_transform_integrand_right (v : V) (w : W) :
-    HasFDerivAt (fun w' ↦ fourierChar [-L v w'] • f v) (fourierChar [-L v w] • mul_L L f v) w := by
+    HasFDerivAt (fun w' ↦ 𝐞 (-L v w') • f v) (𝐞 (-L v w) • mul_L L f v) w := by
   have ha : HasFDerivAt (fun w' : W ↦ L v w') (L v) w := ContinuousLinearMap.hasFDerivAt (L v)
   convert ((hasDerivAt_fourierChar (-L v w)).hasFDerivAt.comp w ha.neg).smul_const (f v)
   ext1 w'
   simp_rw [mul_L, ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply]
   rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.neg_apply,
     ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, ← smul_assoc, smul_comm,
-    ← smul_assoc, real_smul, real_smul, smul_eq_mul]
+    ← smul_assoc, real_smul, real_smul, Submonoid.smul_def, smul_eq_mul]
   push_cast
   ring_nf
 
 /-- Norm of the `w`-derivative of the Fourier transform integrand. -/
 lemma norm_fderiv_fourier_transform_integrand_right
     (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) (w : W) :
-    ‖fourierChar [-L v w] • mul_L L f v‖ = (2 * π) * ‖L v‖ * ‖f v‖ := by
-  rw [norm_smul, norm_eq_abs (fourierChar _ : ℂ), abs_coe_circle, one_mul, mul_L, norm_smul,
-    norm_neg, norm_mul, norm_mul, norm_eq_abs I, abs_I, mul_one, norm_eq_abs ((_ : ℝ) : ℂ),
-    Complex.abs_of_nonneg pi_pos.le, norm_eq_abs (2 : ℂ), Complex.abs_two,
-    ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]
+    ‖𝐞 (-L v w) • mul_L L f v‖ = (2 * π) * ‖L v‖ * ‖f v‖ := by
+  rw [norm_circle_smul, mul_L, norm_smul, norm_neg, norm_mul, norm_mul, norm_eq_abs I, abs_I,
+    mul_one, norm_eq_abs ((_ : ℝ) : ℂ), Complex.abs_of_nonneg pi_pos.le, norm_eq_abs (2 : ℂ),
+    Complex.abs_two, ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]
 
 lemma norm_fderiv_fourier_transform_integrand_right_le (v : V) (w : W) :
-    ‖fourierChar [-L v w] • (mul_L L f v)‖ ≤ (2 * π) * ‖L‖ * ‖v‖ * ‖f v‖ := by
+    ‖𝐞 (-L v w) • (mul_L L f v)‖ ≤ (2 * π) * ‖L‖ * ‖v‖ * ‖f v‖ := by
   rw [norm_fderiv_fourier_transform_integrand_right]
   refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
   conv_rhs => rw [mul_assoc]
@@ -83,22 +78,20 @@ the Fourier transform of `mul_L L f`. -/
 theorem hasFDerivAt_fourier [CompleteSpace E] [MeasurableSpace V] [BorelSpace V] {μ : Measure V}
     [SecondCountableTopologyEither V (W →L[ℝ] ℝ)]
     (hf : Integrable f μ) (hf' : Integrable (fun v : V ↦ ‖v‖ * ‖f v‖) μ) (w : W) :
-    HasFDerivAt (VectorFourier.fourierIntegral fourierChar μ L.toLinearMap₂ f)
-      (VectorFourier.fourierIntegral fourierChar μ L.toLinearMap₂ (mul_L L f) w) w := by
-  let F : W → V → E := fun w' v ↦ fourierChar [-L v w'] • f v
-  let F' : W → V → W →L[ℝ] E := fun w' v ↦ fourierChar [-L v w'] • mul_L L f v
+    HasFDerivAt (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ f)
+      (VectorFourier.fourierIntegral 𝐞 μ L.toLinearMap₂ (mul_L L f) w) w := by
+  let F : W → V → E := fun w' v ↦ 𝐞 (-L v w') • f v
+  let F' : W → V → W →L[ℝ] E := fun w' v ↦ 𝐞 (-L v w') • mul_L L f v
   let B : V → ℝ := fun v ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
   have h0 (w' : W) : Integrable (F w') μ :=
     (VectorFourier.fourier_integral_convergent_iff continuous_fourierChar
       (by apply L.continuous₂ : Continuous (fun p : V × W ↦ L.toLinearMap₂ p.1 p.2)) w').mp hf
   have h1 : ∀ᶠ w' in 𝓝 w, AEStronglyMeasurable (F w') μ :=
     eventually_of_forall (fun w' ↦ (h0 w').aestronglyMeasurable)
-  have h2 : Integrable (F w) μ := h0 w
   have h3 : AEStronglyMeasurable (F' w) μ := by
-    simp only [F']
-    refine AEStronglyMeasurable.smul ?_ ?_
-    · refine (continuous_subtype_val.comp (continuous_fourierChar.comp ?_)).aestronglyMeasurable
-      exact continuous_ofAdd.comp (L.continuous₂.comp (Continuous.Prod.mk_left w)).neg
+    refine .smul ?_ ?_
+    · refine (continuous_fourierChar.comp ?_).aestronglyMeasurable
+      exact (L.continuous₂.comp (Continuous.Prod.mk_left w)).neg
     · apply AEStronglyMeasurable.const_smul'
       have aux0 : Continuous fun p : (W →L[ℝ] ℝ) × E ↦ p.1.smulRight p.2 :=
         (ContinuousLinearMap.smulRightL ℝ W E).continuous₂
@@ -111,7 +104,7 @@ theorem hasFDerivAt_fourier [CompleteSpace E] [MeasurableSpace V] [BorelSpace V]
   have h5 : Integrable B μ := by simpa only [← mul_assoc] using hf'.const_mul (2 * π * ‖L‖)
   have h6 : ∀ᵐ v ∂μ, ∀ w', w' ∈ Metric.ball w 1 → HasFDerivAt (fun x ↦ F x v) (F' w' v) w' :=
     ae_of_all _ (fun v w' _ ↦ hasFDerivAt_fourier_transform_integrand_right L f v w')
-  exact hasFDerivAt_integral_of_dominated_of_fderiv_le one_pos h1 h2 h3 h4 h5 h6
+  exact hasFDerivAt_integral_of_dominated_of_fderiv_le one_pos h1 (h0 w) h3 h4 h5 h6
 
 section inner
 
@@ -120,7 +113,7 @@ variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [SecondCou
 
 /-- Notation for the Fourier transform on a real inner product space -/
 abbrev integralFourier (f : V → E) (μ : Measure V := by volume_tac) :=
-  fourierIntegral fourierChar μ (innerₛₗ ℝ) f
+  fourierIntegral 𝐞 μ (innerₛₗ ℝ) f
 
 /-- The Fréchet derivative of the Fourier transform of `f` is the Fourier transform of
     `fun v ↦ ((-2 * π * I) • f v) ⊗ (innerSL ℝ v)`. -/

Mathlib/Analysis/Fourier/Inversion.lean

@@ -74,12 +74,12 @@ lemma tendsto_integral_gaussian_smul (hf : Integrable f) (h'f : Integrable (𝓕
     atTop (𝓝 (𝓕⁻ (𝓕 f) v)) := by
   have A : Tendsto (fun (c : ℝ) ↦ (∫ w : V, cexp (- c⁻¹ * ‖w‖^2 + 2 * π * I * ⟪v, w⟫)
        • (𝓕 f) w)) atTop (𝓝 (𝓕⁻ (𝓕 f) v)) := by
-    have : Integrable (fun w ↦ 𝐞[⟪w, v⟫] • (𝓕 f) w) := by
+    have : Integrable (fun w ↦ 𝐞 ⟪w, v⟫ • (𝓕 f) w) := by
       have B : Continuous fun p : V × V => (- innerₗ V) p.1 p.2 := continuous_inner.neg
       simpa using
         (VectorFourier.fourier_integral_convergent_iff Real.continuous_fourierChar B v).1 h'f
     convert tendsto_integral_cexp_sq_smul this using 4 with c w
-    · rw [Real.fourierChar_apply, smul_smul, ← Complex.exp_add, real_inner_comm]
+    · rw [Submonoid.smul_def, Real.fourierChar_apply, smul_smul, ← Complex.exp_add, real_inner_comm]
       congr 3
       simp only [ofReal_mul, ofReal_ofNat]
       ring

Mathlib/Analysis/Fourier/PoissonSummation.lean

@@ -62,7 +62,7 @@ theorem Real.fourierCoeff_tsum_comp_add {f : C(ℝ, ℂ)}
   -- block, but I think it's more legible this way. We start with preliminaries about the integrand.
   let e : C(ℝ, ℂ) := (fourier (-m)).comp ⟨((↑) : ℝ → UnitAddCircle), continuous_quotient_mk'⟩
   have neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖(e * g).restrict K‖ = ‖g.restrict K‖ := by
-    have : ∀ x : ℝ, ‖e x‖ = 1 := fun x => abs_coe_circle (AddCircle.toCircle (-m • x))
+    have (x : ℝ) : ‖e x‖ = 1 := abs_coe_circle (AddCircle.toCircle (-m • x))
     intro K g
     simp_rw [norm_eq_iSup_norm, restrict_apply, mul_apply, norm_mul, this, one_mul]
   have eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight n) = e := by

Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

@@ -60,7 +60,7 @@ variable [NormedAddCommGroup V] [MeasurableSpace V] [BorelSpace V] [InnerProduct
 
 /-- The integrand in the Riemann-Lebesgue lemma for `f` is integrable iff `f` is. -/
 theorem fourier_integrand_integrable (w : V) :
-    Integrable f ↔ Integrable fun v : V => 𝐞[-⟪v, w⟫] • f v := by
+    Integrable f ↔ Integrable fun v : V => 𝐞 (-⟪v, w⟫) • f v := by
   have hL : Continuous fun p : V × V => bilinFormOfRealInner p.1 p.2 :=
     continuous_inner
   rw [VectorFourier.fourier_integral_convergent_iff Real.continuous_fourierChar hL w]
@@ -73,35 +73,36 @@ local notation3 "i" => fun (w : V) => (1 / (2 * ‖w‖ ^ 2) : ℝ) • w
 
 /-- Shifting `f` by `(1 / (2 * ‖w‖ ^ 2)) • w` negates the integral in the Riemann-Lebesgue lemma. -/
 theorem fourier_integral_half_period_translate {w : V} (hw : w ≠ 0) :
-    (∫ v : V, 𝐞[-⟪v, w⟫] • f (v + i w)) = -∫ v : V, 𝐞[-⟪v, w⟫] • f v := by
+    (∫ v : V, 𝐞 (-⟪v, w⟫) • f (v + i w)) = -∫ v : V, 𝐞 (-⟪v, w⟫) • f v := by
   have hiw : ⟪i w, w⟫ = 1 / 2 := by
     rw [inner_smul_left, inner_self_eq_norm_sq_to_K, IsROrC.ofReal_real_eq_id, id.def,
       IsROrC.conj_to_real, ← div_div, div_mul_cancel₀]
     rwa [Ne.def, sq_eq_zero_iff, norm_eq_zero]
   have :
-    (fun v : V => 𝐞[-⟪v, w⟫] • f (v + i w)) =
-      fun v : V => (fun x : V => -𝐞[-⟪x, w⟫] • f x) (v + i w) := by
+    (fun v : V => 𝐞 (-⟪v, w⟫) • f (v + i w)) =
+      fun v : V => (fun x : V => -(𝐞 (-⟪x, w⟫) • f x)) (v + i w) := by
     ext1 v
-    simp_rw [inner_add_left, hiw, Real.fourierChar_apply, neg_add, mul_add, ofReal_add, add_mul,
-      exp_add]
+    simp_rw [inner_add_left, hiw, Submonoid.smul_def, Real.fourierChar_apply, neg_add, mul_add,
+      ofReal_add, add_mul, exp_add]
     have : 2 * π * -(1 / 2) = -π := by field_simp; ring
-    rw [this, ofReal_neg, neg_mul, exp_neg, exp_pi_mul_I, inv_neg, inv_one, mul_neg_one, neg_neg]
+    rw [this, ofReal_neg, neg_mul, exp_neg, exp_pi_mul_I, inv_neg, inv_one, mul_neg_one, neg_smul,
+      neg_neg]
   rw [this]
   -- Porting note:
   -- The next three lines had just been
   -- rw [integral_add_right_eq_self (fun (x : V) ↦ -(𝐞[-⟪x, w⟫]) • f x)
   --       ((fun w ↦ (1 / (2 * ‖w‖ ^ (2 : ℕ))) • w) w)]
-  -- Unfortunately now we need to specify `volume`, and call `dsimp`.
-  have := @integral_add_right_eq_self _ _ _ _ _ volume _ _ _ (fun (x : V) ↦ -(𝐞[-⟪x, w⟫]) • f x)
+  -- Unfortunately now we need to specify `volume`.
+  have := integral_add_right_eq_self (μ := volume) (fun (x : V) ↦ -(𝐞 (-⟪x, w⟫) • f x))
     ((fun w ↦ (1 / (2 * ‖w‖ ^ (2 : ℕ))) • w) w)
-  erw [this] -- Porting note, we can avoid `erw` by first calling `dsimp at this ⊢`.
+  rw [this]
   simp only [neg_smul, integral_neg]
 #align fourier_integral_half_period_translate fourier_integral_half_period_translate
 
 /-- Rewrite the Fourier integral in a form that allows us to use uniform continuity. -/
 theorem fourier_integral_eq_half_sub_half_period_translate {w : V} (hw : w ≠ 0)
     (hf : Integrable f) :
-    ∫ v : V, 𝐞[-⟪v, w⟫] • f v = (1 / (2 : ℂ)) • ∫ v : V, 𝐞[-⟪v, w⟫] • (f v - f (v + i w)) := by
+    ∫ v : V, 𝐞 (-⟪v, w⟫) • f v = (1 / (2 : ℂ)) • ∫ v : V, 𝐞 (-⟪v, w⟫) • (f v - f (v + i w)) := by
   simp_rw [smul_sub]
   rw [integral_sub, fourier_integral_half_period_translate hw, sub_eq_add_neg, neg_neg, ←
     two_smul ℂ _, ← @smul_assoc _ _ _ _ _ _ (IsScalarTower.left ℂ), smul_eq_mul]
@@ -116,9 +117,9 @@ of interest as a preparatory step for the more general result
 `tendsto_integral_exp_inner_smul_cocompact` in which `f` can be arbitrary. -/
 theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support (hf1 : Continuous f)
     (hf2 : HasCompactSupport f) :
-    Tendsto (fun w : V => ∫ v : V, 𝐞[-⟪v, w⟫] • f v) (cocompact V) (𝓝 0) := by
+    Tendsto (fun w : V => ∫ v : V, 𝐞 (-⟪v, w⟫) • f v) (cocompact V) (𝓝 0) := by
   refine' NormedAddCommGroup.tendsto_nhds_zero.mpr fun ε hε => _
-  suffices ∃ T : ℝ, ∀ w : V, T ≤ ‖w‖ → ‖∫ v : V, 𝐞[-⟪v, w⟫] • f v‖ < ε by
+  suffices ∃ T : ℝ, ∀ w : V, T ≤ ‖w‖ → ‖∫ v : V, 𝐞 (-⟪v, w⟫) • f v‖ < ε by
     simp_rw [← comap_dist_left_atTop_eq_cocompact (0 : V), eventually_comap, eventually_atTop,
       dist_eq_norm', sub_zero]
     exact
@@ -156,7 +157,7 @@ theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support
       (hf1.integrable_of_hasCompactSupport hf2),
     norm_smul, this, inv_mul_eq_div, div_lt_iff' two_pos]
   refine' lt_of_le_of_lt (norm_integral_le_integral_norm _) _
-  simp_rw [norm_smul, norm_eq_abs, abs_coe_circle, one_mul]
+  simp_rw [norm_circle_smul]
   --* Show integral can be taken over A only.
   have int_A : ∫ v : V, ‖f v - f (v + i w)‖ = ∫ v in A, ‖f v - f (v + i w)‖ := by
     refine' (set_integral_eq_integral_of_forall_compl_eq_zero fun v hv => _).symm
@@ -205,7 +206,7 @@ variable (f)
 /-- Riemann-Lebesgue lemma for functions on a real inner-product space: the integral
 `∫ v, exp (-2 * π * ⟪w, v⟫ * I) • f v` tends to 0 as `w → ∞`. -/
 theorem tendsto_integral_exp_inner_smul_cocompact :
-    Tendsto (fun w : V => ∫ v, 𝐞[-⟪v, w⟫] • f v) (cocompact V) (𝓝 0) := by
+    Tendsto (fun w : V => ∫ v, 𝐞 (-⟪v, w⟫) • f v) (cocompact V) (𝓝 0) := by
   by_cases hfi : Integrable f; swap
   · convert tendsto_const_nhds (x := (0 : E)) with w
     apply integral_undef
@@ -220,15 +221,12 @@ theorem tendsto_integral_exp_inner_smul_cocompact :
           _ (div_pos hε two_pos)).mp
       (eventually_of_forall fun w hI => _)
   rw [dist_eq_norm] at hI ⊢
-  have : ‖(∫ v, 𝐞[-⟪v, w⟫] • f v) - ∫ v, 𝐞[-⟪v, w⟫] • g v‖ ≤ ε / 2 := by
+  have : ‖(∫ v, 𝐞 (-⟪v, w⟫) • f v) - ∫ v, 𝐞 (-⟪v, w⟫) • g v‖ ≤ ε / 2 := by
     refine' le_trans _ hfg
-    simp_rw [←
-      integral_sub ((fourier_integrand_integrable w).mp hfi)
+    simp_rw [← integral_sub ((fourier_integrand_integrable w).mp hfi)
         ((fourier_integrand_integrable w).mp (hg_cont.integrable_of_hasCompactSupport hg_supp)),
       ← smul_sub, ← Pi.sub_apply]
-    exact
-      VectorFourier.norm_fourierIntegral_le_integral_norm 𝐞 volume
-        (bilinFormOfRealInner) (f - g) w
+    exact VectorFourier.norm_fourierIntegral_le_integral_norm 𝐞 _ bilinFormOfRealInner (f - g) w
   replace := add_lt_add_of_le_of_lt this hI
   rw [add_halves] at this
   refine' ((le_of_eq _).trans (norm_add_le _ _)).trans_lt this
@@ -237,7 +235,7 @@ theorem tendsto_integral_exp_inner_smul_cocompact :
 
 /-- The Riemann-Lebesgue lemma for functions on `ℝ`. -/
 theorem Real.tendsto_integral_exp_smul_cocompact (f : ℝ → E) :
-    Tendsto (fun w : ℝ => ∫ v : ℝ, 𝐞[-(v * w)] • f v) (cocompact ℝ) (𝓝 0) :=
+    Tendsto (fun w : ℝ => ∫ v : ℝ, 𝐞 (-(v * w)) • f v) (cocompact ℝ) (𝓝 0) :=
   tendsto_integral_exp_inner_smul_cocompact f
 #align real.tendsto_integral_exp_smul_cocompact Real.tendsto_integral_exp_smul_cocompact
 
@@ -250,19 +248,18 @@ theorem Real.zero_at_infty_fourierIntegral (f : ℝ → E) : Tendsto (𝓕 f) (c
 via dual space. **Do not use** -- it is only a stepping stone to
 `tendsto_integral_exp_smul_cocompact` where the inner-product-space structure isn't required. -/
 theorem tendsto_integral_exp_smul_cocompact_of_inner_product (μ : Measure V) [μ.IsAddHaarMeasure] :
-    Tendsto (fun w : V →L[ℝ] ℝ => ∫ v, 𝐞[-w v] • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0) := by
+    Tendsto (fun w : V →L[ℝ] ℝ => ∫ v, 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0) := by
   rw [μ.isAddLeftInvariant_eq_smul volume]
   simp_rw [integral_smul_nnreal_measure]
   rw [← (smul_zero _ : Measure.addHaarScalarFactor μ volume • (0 : E) = 0)]
   apply Tendsto.const_smul
   let A := (InnerProductSpace.toDual ℝ V).symm
-  have : (fun w : V →L[ℝ] ℝ => ∫ v, 𝐞[-w v] • f v) = (fun w : V => ∫ v, 𝐞[-⟪v, w⟫] • f v) ∘ A := by
+  have : (fun w : V →L[ℝ] ℝ ↦ ∫ v, 𝐞 (-w v) • f v) = (fun w : V ↦ ∫ v, 𝐞 (-⟪v, w⟫) • f v) ∘ A := by
     ext1 w
     congr 1 with v : 1
     rw [← inner_conj_symm, IsROrC.conj_to_real, InnerProductSpace.toDual_symm_apply]
   rw [this]
-  exact
-    (tendsto_integral_exp_inner_smul_cocompact f).comp
+  exact (tendsto_integral_exp_inner_smul_cocompact f).comp
       A.toHomeomorph.toCocompactMap.cocompact_tendsto'
 #align tendsto_integral_exp_smul_cocompact_of_inner_product tendsto_integral_exp_smul_cocompact_of_inner_product
 
@@ -277,7 +274,7 @@ variable (f) [AddCommGroup V] [TopologicalSpace V] [TopologicalAddGroup V] [T2Sp
 /-- Riemann-Lebesgue lemma for functions on a finite-dimensional real vector space, formulated via
 dual space. -/
 theorem tendsto_integral_exp_smul_cocompact (μ : Measure V) [μ.IsAddHaarMeasure] :
-    Tendsto (fun w : V →L[ℝ] ℝ => ∫ v, 𝐞[-w v] • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0) := by
+    Tendsto (fun w : V →L[ℝ] ℝ => ∫ v, 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0) := by
   -- We have already proved the result for inner-product spaces, formulated in a way which doesn't
   -- refer to the inner product. So we choose an arbitrary inner-product space isomorphic to V
   -- and port the result over from there.