English
Let V and W be normed spaces over the real numbers, and let L be a continuous bilinear map that assigns a real number to a pair (v, w) with v ∈ V and w ∈ W. Consider the complex-valued function v ↦ e^{ - L(v, w) } (viewed as a Fourier character). Then the Fréchet derivative of this function with respect to v in the direction y is given by the complex scalar -2π i · L(y, w) multiplied by e^{ - L(v, w) }.
Русский
Пусть V и W — нормированные пространства над R, пусть L — непрерывно-билинейное отображение, связывающее пару (v, w) с вещественным числом, v ∈ V, w ∈ W. Рассматривая функцию v ↦ e^{ - L(v, w) } как комплексную характеристическую функцию Фурье, ее фредхелевское приближение по направлению y равно -2π i · L(y, w) · e^{ - L(v, w) }.
LaTeX
$$$D_v\\left( e^{-L(v,w)} \right)[y] \;=\; -2\\pi i \\; L(y,w)\\, e^{-L(v,w)}$$$
Lean4
theorem fderiv_fourierChar_neg_bilinear_left_apply (v y : V) (w : W) :
fderiv ℝ (fun v ↦ (𝐞 (-L v w) : ℂ)) v y = -2 * π * I * L y w * 𝐞 (-L v w) :=
by
simp only [(hasFDerivAt_fourierChar_neg_bilinear_left L v w).fderiv, neg_mul, ContinuousLinearMap.coe_smul',
ContinuousLinearMap.coe_comp', Pi.smul_apply, Function.comp_apply, ContinuousLinearMap.flip_apply, ofRealCLM_apply,
smul_eq_mul, neg_inj]
ring
