English
The Fourier integral of the n-th derivative of iteratedFDeriv relates to the iterated Fourier integral of f via a right-multiplication by a weight given by fourierPowSMulRight on f.
Русский
Интеграл Фурье от n-й производной от iteratedFDeriv связывается с итеративным Фурье-интегралом f через правый множитель-услаг weight fourierPowSMulRight.
LaTeX
$$$$ \mathcal{F}\bigl( \mathrm{iteratedFDeriv}_{\mathbb{R}}^{n}( f ) \bigr) = \mathcal{F} f \; \text{смещённое по весу} \; w \; n $$$$
Lean4
/-- The Fourier integral of the `n`-th derivative of a function is obtained by multiplying the
Fourier integral of the original function by `(2πI L w ⬝ )^n`. -/
theorem fourierIntegral_iteratedFDeriv {N : ℕ∞} (hf : ContDiff ℝ N f)
(h'f : ∀ (n : ℕ), n ≤ N → Integrable (iteratedFDeriv ℝ n f)) {n : ℕ} (hn : n ≤ N) :
𝓕 (iteratedFDeriv ℝ n f) = (fun w ↦ fourierPowSMulRight (-innerSL ℝ) (𝓕 f) w n) :=
by
rw [← innerSL_real_flip V]
exact VectorFourier.fourierIntegral_iteratedFDeriv (innerSL ℝ) hf h'f hn
