fourierSMulRight — Mathlib

English

For fixed v ∈ V and w ∈ W, the map w ↦ e^{ - L(v,w) } · f(v) has a well-defined Fréchet derivative with respect to w at w, expressed in terms of L and f.

Русский

Для фиксированного v ∈ V и w ∈ W функция w ↦ e^{ - L(v,w) } · f(v) имеет корректную фрет-деративу по w в точке w, выражаемую через L и f.

LaTeX

$$$\\text{HasFDerivAt}\\big( w \\mapsto e^{ -L(v,w) } \\cdot f(v) \\big)\\,$$

Lean4

/-- Send a function `f : V → E` to the function `f : V → Hom (W, E)` given by
`v ↦ (w ↦ -2 * π * I * L (v, w) • f v)`. This is designed so that the Fourier transform of
`fourierSMulRight L f` is the derivative of the Fourier transform of `f`. -/
def fourierSMulRight (v : V) : (W →L[ℝ] E) :=
  -(2 * π * I) • (L v).smulRight (f v)

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