English
Shifting the input by a left-translation corresponds to multiplying the Fourier integral by a phase factor depending on the shift and 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 transform converts right-translation into scalar multiplication by a phase
factor. -/
theorem fourierIntegral_comp_add_right [MeasurableAdd 𝕜] (e : AddChar 𝕜 𝕊) (μ : Measure 𝕜) [μ.IsAddRightInvariant]
(f : 𝕜 → E) (v₀ : 𝕜) : fourierIntegral e μ (f ∘ fun v ↦ v + v₀) = fun w ↦ e (v₀ * w) • fourierIntegral e μ f w :=
VectorFourier.fourierIntegral_comp_add_right _ _ _ _ _
