fderiv_fourierChar_neg_bilinear_right_apply

English

The derivative of the map w ↦ 𝐞^{−L(v,w)} with respect to w in direction y is −2π i L v y 𝐞^{−L(v,w)}.

Русский

Производная по переменной w в направлении y равна −2π i L v y 𝐞^{−L(v,w)}.

LaTeX

$$$fderiv\\,\\mathbb{R}\\ (w \\mapsto 𝐞^{−L(v,w)})\\; y = -2 \\pi i \\; L v y \\; 𝐞^{−L(v,w)}$$$

Lean4

theorem fderiv_fourierChar_neg_bilinear_right_apply (v : V) (w y : W) :
    fderiv ℝ (fun w ↦ (𝐞 (-L v w) : ℂ)) w y = -2 * π * I * L v y * 𝐞 (-L v w) :=
  by
  simp only [(hasFDerivAt_fourierChar_neg_bilinear_right L v w).fderiv, neg_mul, ContinuousLinearMap.coe_smul',
    ContinuousLinearMap.coe_comp', Pi.smul_apply, Function.comp_apply, ofRealCLM_apply, smul_eq_mul, neg_inj]
  ring

Похожие утверждения