hasFDerivAt_fourierChar_neg_bilinear_left

English

Both left and right bilinear derivatives exist; they give the same bilinear differential expression with L and L.flip.

Русский

Существуют слева и справа производные билинейной части; обе дают одно и то же дифференциальное выражение через L и L.flip.

LaTeX

$$$\\text{HasFDerivAt}_{L}(v,w) = \\text{HasFDerivAt}_{L.flip}(v,w)$$$

Lean4

theorem hasFDerivAt_fourierChar_neg_bilinear_left (v : V) (w : W) :
    HasFDerivAt (fun v ↦ (𝐞 (-L v w) : ℂ)) ((-2 * π * I * 𝐞 (-L v w)) • (ofRealCLM ∘L (L.flip w))) v :=
  hasFDerivAt_fourierChar_neg_bilinear_right L.flip w v

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