fourierTransformCLE_symm_apply — Mathlib

English

The Fourier CLE symm applies to give the opposite transform: (fourierTransformCLE 𝕜).symm f = 𝓕⁻ f.

Русский

У слева симметрия Фурье CLE: (fourierTransformCLE 𝕜).symm f = 𝓕⁻ f.

LaTeX

$$$ (\mathrm{fourierTransformCLE}_{\mathbb{K}})^{-1}(f) = \mathcal{F}^{-} f $$$

Lean4

@[simp]
theorem fourierTransformCLE_symm_apply (f : 𝓢(V, E)) : (fourierTransformCLE 𝕜).symm f = 𝓕⁻ f :=
  by
  ext x
  exact (fourierIntegralInv_eq_fourierIntegral_neg f x).symm

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