English
When integrating a parameterized family, the Fourier integral has a Fréchet derivative with respect to the parameter, and this derivative is the Fourier transform of the derivative family given by fourierSMulRight L f.
Русский
При интегрировании параметрически зависимой семьи Фурье-интеграл имеет фрет-деративу по параметру; производная равна Фурье-преобразованию производной семьи через fourierSMulRight L f.
LaTeX
$$$\\text{HasFDerivAt}\\left( \\text{fourierIntegral } 𝐞 μ L f,\\; w \\right) = \\text{fourierIntegral } 𝐞 μ L (\\text{fourierSMulRight } L f) w$$$
Lean4
theorem norm_fourierSMulRight_le (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) :
‖fourierSMulRight L f v‖ ≤ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖ :=
calc
‖fourierSMulRight L f v‖ = (2 * π) * ‖L v‖ * ‖f v‖ := norm_fourierSMulRight _ _ _
_ ≤ (2 * π) * (‖L‖ * ‖v‖) * ‖f v‖ := by gcongr; exact L.le_opNorm _
_ = 2 * π * ‖L‖ * ‖v‖ * ‖f v‖ := by ring
