differentiable_fourierChar_neg_bilinear_right

English

The left bilinear derivative exists and equals the same formal expression via L.flip.

Русский

Слевая билинейная производная существует и совпадает с выражением через L.flip.

LaTeX

$$$\\text{HasFDerivAt} (f) = \\text{HasFDerivAt} (f \\circ (\\text{flip}))$$$

Lean4

theorem differentiable_fourierChar_neg_bilinear_right (v : V) : Differentiable ℝ (fun w ↦ (𝐞 (-L v w) : ℂ)) := fun w ↦
  (hasFDerivAt_fourierChar_neg_bilinear_right L v w).differentiableAt

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