English
There exists a Taylor series up to any finite order N (in the sense of HasFTaylorSeriesUpTo) for the Fourier integral, with the nth term given by the corresponding FourierPowSMulRight terms.
Русский
Существует ряд Тейлора до порядка N для Фурье-интеграла, где n-й член задаётся соответствующими членами FourierPowSMulRight.
LaTeX
$$$\\text{HasFTaylorSeriesUpTo}\\; N\\; (\\text{fourierIntegral } ...)\\; (\\text{fun } w\\; n \\mapsto \\text{fourierIntegral } ... (\\text{fourierPowSMulRight } L f v n) w)$$$
Lean4
theorem _root_.ContDiff.fourierPowSMulRight {f : V → E} {k : WithTop ℕ∞} (hf : ContDiff ℝ k f) (n : ℕ) :
ContDiff ℝ k (fun v ↦ fourierPowSMulRight L f v n) :=
by
simp_rw [fourierPowSMulRight_eq_comp]
apply ContDiff.const_smul
apply (smulRightL ℝ (fun (_ : Fin n) ↦ W) E).isBoundedBilinearMap.contDiff.comp₂ _ hf
apply (ContinuousMultilinearMap.contDiff _).comp
exact contDiff_pi.2 (fun _ ↦ L.contDiff)
