English
If f is continuously differentiable and all relevant derivatives exist, then the map v ↦ fourierPowSMulRight L f v n is continuously differentiable in v (as a function into E).
Русский
Если f непрерывно Дифференцируема, а все соответствующие производные существуют, то v ↦ fourierPowSMulRight L f v n является непрерывно дифференцируемой по v (в пространство E).
LaTeX
$$$\\text{ContDiff}_{\\mathbb{R}}\\; k\\; (v \\mapsto \\text{fourierPowSMulRight } L f v n)$$$
Lean4
/-- The formal multilinear series whose `n`-th term is
`(w₁, ..., wₙ) ↦ (-2πI)^n * L v w₁ * ... * L v wₙ • f v`, as a continuous multilinear map in
the space `W [×n]→L[ℝ] E`.
This is designed so that the Fourier transform of `v ↦ fourierPowSMulRight L f v n` is the
`n`-th derivative of the Fourier transform of `f`.
-/
def fourierPowSMulRight (f : V → E) (v : V) : FormalMultilinearSeries ℝ W E := fun n ↦
(-(2 * π * I)) ^ n •
((ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (f v)).compContinuousLinearMap (fun _ ↦ L v))
/- Increase the priority to make sure that this lemma is used instead of
`FormalMultilinearSeries.apply_eq_prod_smul_coeff` even in dimension 1. -/
