English
Shifting f by the vector i w along an inner-product space negates the Fourier integral up to a sign: the integral of e^{-⟨v,w⟩} f(v+i w) dv equals minus the integral of e^{-⟨v,w⟩} f(v) dv, up to the same exponential kernel.
Русский
Смещение f на вектор i w меняет знак интеграла Фурье: интеграл e^{-⟨v,w⟩} f(v+i w) dv равен минус интеграла e^{-⟨v,w⟩} f(v) dv.
LaTeX
$$$(\\forall w\\neq 0)\\; \\int_V e^{-⟨v,w⟩} f(v+i w) \\; dv = -\\int_V e^{-⟨v,w⟩} f(v) \\; dv$$$
Lean4
/-- Shifting `f` by `(1 / (2 * ‖w‖ ^ 2)) • w` negates the integral in the Riemann-Lebesgue lemma. -/
theorem fourierIntegral_half_period_translate {w : V} (hw : w ≠ 0) :
(∫ v : V, 𝐞 (-⟪v, w⟫) • f (v + i w)) = -∫ v : V, 𝐞 (-⟪v, w⟫) • f v :=
by
have hiw : ⟪i w, w⟫ = 1 / 2 :=
by
rw [inner_smul_left, inner_self_eq_norm_sq_to_K, RCLike.ofReal_real_eq_id, id, RCLike.conj_to_real, ← div_div,
div_mul_cancel₀]
rwa [Ne, sq_eq_zero_iff, norm_eq_zero]
have : (fun v : V => 𝐞 (-⟪v, w⟫) • f (v + i w)) = fun v : V => (fun x : V => -(𝐞 (-⟪x, w⟫) • f x)) (v + i w) :=
by
ext1 v
simp_rw [inner_add_left, hiw, Circle.smul_def, Real.fourierChar_apply, neg_add, mul_add, ofReal_add, add_mul,
exp_add]
have : 2 * π * -(1 / 2) = -π := by field_simp
rw [this, ofReal_neg, neg_mul, exp_neg, exp_pi_mul_I, inv_neg, inv_one, mul_neg_one, neg_smul, neg_neg]
rw [this, integral_add_right_eq_self (fun (x : V) ↦ -(𝐞 (-⟪x, w⟫) • f x)) ((fun w ↦ (1 / (2 * ‖w‖ ^ (2 : ℕ))) • w) w)]
simp only [integral_neg]
