no goals
E✝ : Type ?u.2407652
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : CompleteSpace E✝
inst✝³ : NormedSpace ℂ E✝
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ 𝓕 f w = ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v
simp_rw [fourierIntegral_def, Real.fourierChar_apply, mul_neg, neg_mul, mul_assoc]