English
If f and g are integrable, then the inner product of their Fourier transforms equals the inner product of f and the Fourier transform of g, reflecting self-adjointness under the bilinear pairing.
Русский
Если f и g интегрируемы, то скалярное произведение их преобразований Фурье равняется скалярному произведению самих функций и преобразования Фурье другой функции, демонстрируя самопряженность под билинейной связью.
LaTeX
$$$$ \\int g(\\xi) \\overline{\\mathrm{fourierIntegral}(f)(\\xi)} \\, d\\nu(\\xi) = \\int f(x) \\overline{\\mathrm{fourierIntegral}(g)(x)} \\, d\\mu(x). $$$$
Lean4
theorem fourierIntegral_probChar {V W : Type*} {_ : MeasurableSpace V} [AddCommGroup V] [Module ℝ V] [AddCommGroup W]
[Module ℝ W] (L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ) (μ : Measure V) (f : V → E) (w : W) :
fourierIntegral Real.probChar μ L f w = ∫ v : V, Complex.exp (-L v w * Complex.I) • f v ∂μ := by
simp_rw [fourierIntegral, Circle.smul_def, Real.probChar_apply, Complex.ofReal_neg]
