English
The Fourier integral commutes with translations in the input, yielding a phase factor times the original transform at the shifted frequency.
Русский
Преобразование Фурье сохраняет перевод входной функции через фазовый множитель и соответствующее смещение частоты.
LaTeX
$$$$ \\mathrm{fourierIntegral}(e, μ, L, f(\\cdot + v_0))(w) = e(L(v_0,w)) \\cdot \\mathrm{fourierIntegral}(e, μ, L, f)(w). $$$$
Lean4
/-- The Fourier integral is well defined iff the function is integrable. Version with a general
continuous bilinear function `L`. For the specialization to the inner product in an inner product
space, see `Real.fourierIntegral_convergent_iff`. -/
@[simp]
theorem fourierIntegral_convergent_iff' {V W : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W]
[NormedSpace ℝ W] [MeasurableSpace V] [BorelSpace V] {μ : Measure V} {f : V → E} (L : V →L[ℝ] W →L[ℝ] ℝ) (w : W) :
Integrable (fun v : V ↦ 𝐞 (-L v w) • f v) μ ↔ Integrable f μ :=
VectorFourier.fourierIntegral_convergent_iff (E := E) (L := L.toLinearMap₁₂) continuous_fourierChar L.continuous₂ _
