English
The n-th Fourier power-smul-right can be decomposed as a scalar factor times a composition of a multilinear map mkPiAlgebra with L.
Русский
n-я степень-фурье-умножение справа разбивается на скалярный коэффициент и композицию много линейной карты mkPiAlgebra с L.
LaTeX
$$$fourierPowSMulRight\\; L\\; f\\; v\\; n = (-2\\pi i)^n \\cdot smulRightL\\; \\mathbb{R}\\; (\\lambda i. L v (i)) \\; (f v)$$$
Lean4
/-- Decomposing `fourierPowSMulRight L f v n` as a composition of continuous bilinear and
multilinear maps, to deduce easily its continuity and differentiability properties. -/
theorem fourierPowSMulRight_eq_comp {f : V → E} {v : V} {n : ℕ} :
fourierPowSMulRight L f v n =
(-(2 * π * I)) ^ n •
smulRightL ℝ (fun (_ : Fin n) ↦ W) E
(compContinuousLinearMapLRight (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) (fun _ ↦ L v)) (f v) :=
rfl
