English
The w-derivative of the Fourier transform integrand, viewed as a function of w, exists and is given by the action of the derivative of the exponential Fourier character on the smulRight of f by L(v), in a bilinear fashion.
Русский
Существуют производные по переменной w интегранта Фурье, и они задаются через производную экспоненциальной фурье-части на смулу по L(v).
LaTeX
$$$\\text{HasFDerivAt}\\left( w' \\mapsto e^{ -L(v,w') } \\cdot f(v) \\right)\\, w \\;=\\; \\text{(орм)}$$$
Lean4
/-- The `w`-derivative of the Fourier transform integrand. -/
theorem hasFDerivAt_fourierChar_smul (v : V) (w : W) :
HasFDerivAt (fun w' ↦ 𝐞 (-L v w') • f v) (𝐞 (-L v w) • fourierSMulRight L f v) w :=
by
have ha : HasFDerivAt (fun w' : W ↦ L v w') (L v) w := ContinuousLinearMap.hasFDerivAt (L v)
convert ((hasDerivAt_fourierChar (-L v w)).hasFDerivAt.comp w ha.neg).smul_const (f v)
ext w' : 1
simp_rw [fourierSMulRight, ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply]
rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.neg_apply, ContinuousLinearMap.smulRight_apply,
ContinuousLinearMap.one_apply, ← smul_assoc, smul_comm, ← smul_assoc, real_smul, real_smul, Submonoid.smul_def,
smul_eq_mul]
push_cast
ring_nf
