fourierIntegral_eq' — Mathlib

English

The Fourier transform of the composition with a linear isometry A satisfies 𝓕 (f ∘ A) w = (𝓕 f) (A w).

Русский

Преобразование Фурье при композиции с линейной изометрией сохраняет форму: 𝓕 (f ∘ A) w = 𝓕 f (A w).

LaTeX

$$$\\mathcal{F} (f \\circ A) w = (\\mathcal{F} f)(A w)$$$

Lean4

theorem fourierIntegral_eq' (f : V → E) (w : V) : 𝓕 f w = ∫ v, Complex.exp ((↑(-2 * π * ⟪v, w⟫) * Complex.I)) • f v :=
  by simp_rw [fourierIntegral_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul]

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