hasDerivAt_fourierChar — Mathlib

English

The Fourier character exp is differentiable with derivative 2π i e^{2π i x} at any real x.

Русский

Фурье-символ e^{2π i x} дифференцируем в любой точке x и имеет производную 2π i e^{2π i x}.

LaTeX

$$$\\operatorname{HasDerivAt} (𝐞 · : \\mathbb{R} \\to \\mathbb{C}) \\; (2\\pi i) \\; 𝐞 x$$$

Lean4

theorem hasDerivAt_fourierChar (x : ℝ) : HasDerivAt (𝐞 · : ℝ → ℂ) (2 * π * I * 𝐞 x) x :=
  by
  have h1 (y : ℝ) : 𝐞 y = fourier 1 (y : UnitAddCircle) :=
    by
    rw [fourierChar_apply, fourier_coe_apply]
    push_cast
    ring_nf
  simpa only [h1, Int.cast_one, ofReal_one, div_one, mul_one] using hasDerivAt_fourier 1 1 x

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