English
More generally, translating the input of the Fourier integral by v0 yields a phase factor given by e(L v0 w) multiplying the original transform evaluated at w.
Русский
В более общем виде сдвиг входа преобразования Фурье на v0 дает фазовый множитель e(L v0 w), который умножает исходное преобразование при частоте w.
LaTeX
$$$$ \\mathrm{fourierIntegral}(e, \\mu, L, f \\circ (\\cdot + v_0))(w) = e( L(v_0, w) ) \\cdot \\mathrm{fourierIntegral}(e, \\mu, L, f)(w). $$$$
Lean4
/-- The Fourier integral converts right-translation into scalar multiplication by a phase factor. -/
theorem fourierIntegral_comp_add_right [MeasurableAdd V] (e : AddChar 𝕜 𝕊) (μ : Measure V) [μ.IsAddRightInvariant]
(L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (v₀ : V) :
fourierIntegral e μ L (f ∘ fun v ↦ v + v₀) = fun w ↦ e (L v₀ w) • fourierIntegral e μ L f w :=
by
ext1 w
dsimp only [fourierIntegral, Function.comp_apply, Circle.smul_def]
conv in L _ => rw [← add_sub_cancel_right v v₀]
rw [integral_add_right_eq_self fun v : V ↦ (e (-L (v - v₀) w) : ℂ) • f v, ← integral_smul]
congr 1 with v
rw [← smul_assoc, smul_eq_mul, ← Circle.coe_mul, ← e.map_add_eq_mul, ← LinearMap.neg_apply, ← sub_eq_add_neg, ←
LinearMap.sub_apply, LinearMap.map_sub, neg_sub]
