English
The n-th Fourier power-smul right is given by a scalar factor times the product over i of L v (m i) and f(v).
Русский
n-я степенная фурье-умножение справа равно скалярному коэффициенту, умноженному на произведение по i от L(v, m i) и f(v).
LaTeX
$$$fourierPowSMulRight\\; L\\; f\\; v\\; n = (-2\\pi i)^n \\cdot \\Big( \\prod_{i=1}^n L(v, m_i) \\Big) \\cdot f(v)$$$
Lean4
/-- The Fourier integral of the derivative of a function is obtained by multiplying the Fourier
integral of the original function by `-L w v`. -/
theorem fourierIntegral_fderiv [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] {μ : Measure V}
[Measure.IsAddHaarMeasure μ] (hf : Integrable f μ) (h'f : Differentiable ℝ f) (hf' : Integrable (fderiv ℝ f) μ) :
fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fderiv ℝ f) =
fourierSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) :=
by
ext w y
let g (v : V) : ℂ :=
𝐞
(-L v w)
/- First rewrite things in a simplified form, without any real change. -/
suffices ∫ x, g x • fderiv ℝ f x y ∂μ = ∫ x, (2 * ↑π * I * L y w * g x) • f x ∂μ
by
rw [fourierIntegral_continuousLinearMap_apply' hf']
simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply, fourierSMulRight_apply,
ContinuousLinearMap.neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul, smul_neg, ← smul_smul,
coe_smul, neg_neg]
-- Key step: integrate by parts with respect to `y` to switch the derivative from `f` to `g`.
have A x : fderiv ℝ g x y = -2 * ↑π * I * L y w * g x := fderiv_fourierChar_neg_bilinear_left_apply _ _ _ _
rw [integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable, ← integral_neg]
· simp only [A, neg_mul, neg_smul, neg_neg]
· have : Integrable (fun x ↦ (-(2 * ↑π * I * ↑((L y) w)) • ((g x : ℂ) • f x))) μ :=
((fourierIntegral_convergent_iff' _ _).2 hf).smul _
convert this using 2 with x
simp only [A, neg_mul, neg_smul, smul_smul]
· exact (fourierIntegral_convergent_iff' _ _).2 (hf'.apply_continuousLinearMap _)
· exact (fourierIntegral_convergent_iff' _ _).2 hf
· exact differentiable_fourierChar_neg_bilinear_left _ _
· exact h'f
