no goals
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedSpace ℂ E
V : Type u_1
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
inst✝² : MeasurableSpace V
W : Type u_2
inst✝¹ : AddCommGroup W
inst✝ : Module ℝ W
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
μ : MeasureTheory.Measure V
f : V → E
w : W
⊢ VectorFourier.fourierIntegral fourierChar μ L f w =
    ∫ (v : V), Complex.exp (↑(-2 * π * ↑(↑L v) w) * Complex.I) • f v ∂μ
simp_rw [VectorFourier.fourierIntegral, Real.fourierChar_apply, mul_neg, neg_mul]