differentiable_fourierChar_neg_bilinear_left

English

The map v ↦ 𝐞^{ - L(v,w) } (viewed as a complex-valued Fourier character) is differentiable with respect to v for every fixed w ∈ W.

Русский

Отображение v ↦ 𝐞^{ - L(v,w) } (комплексная характеристическая функция Фурье) дифференцируемо по переменной v для каждого фиксированного w ∈ W.

LaTeX

$$$\\text{Differentiable}_{\\mathbb{R}}\\big( v \\mapsto (e^{ -L(v,w)}) \\big)$$$

Lean4

theorem differentiable_fourierChar_neg_bilinear_left (w : W) : Differentiable ℝ (fun v ↦ (𝐞 (-L v w) : ℂ)) := fun v ↦
  (hasFDerivAt_fourierChar_neg_bilinear_left L v w).differentiableAt

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