Fourier pairings and Parseval on Schwartz functions

These identities concern the ordinary Fourier integral on Euclidean space. They use Fourier inversion on Schwartz functions, without introducing an extension of the Fourier transform to all of L².

theorem NavierStokesR3.SchwartzParseval.integral_fourier_mul {f g : ProblemStatement.Space → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : ∫ (ξ : ProblemStatement.Space), FourierTransform.fourier f ξ * g ξ = ∫ (x : ProblemStatement.Space), f x * FourierTransform.fourier g x

Fourier duality for two integrable complex functions.

theorem NavierStokesR3.SchwartzParseval.fourier_conj_apply (f : ProblemStatement.Space → ℂ) (ξ : ProblemStatement.Space) : FourierTransform.fourier (fun (x : ProblemStatement.Space) => (starRingEnd ℂ) (f x)) ξ = (starRingEnd ℂ) (FourierTransformInv.fourierInv f ξ)

Conjugation changes the sign in the Fourier kernel.

theorem NavierStokesR3.SchwartzParseval.integral_fourier_mul_conj (f g : Comparison.ComplexTest) : ∫ (ξ : ProblemStatement.Space), FourierTransform.fourier (⇑f) ξ * (starRingEnd ℂ) (FourierTransform.fourier (⇑g) ξ) = ∫ (x : ProblemStatement.Space), f x * (starRingEnd ℂ) (g x)

The Hermitian pairing of two Schwartz functions is preserved by Fourier transform.

theorem NavierStokesR3.SchwartzParseval.integral_conj_fourier_mul (f g : Comparison.ComplexTest) : ∫ (ξ : ProblemStatement.Space), (starRingEnd ℂ) (FourierTransform.fourier (⇑f) ξ) * FourierTransform.fourier (⇑g) ξ = ∫ (x : ProblemStatement.Space), (starRingEnd ℂ) (f x) * g x

The convention with conjugation on the first factor, used by complex inner products.

theorem NavierStokesR3.SchwartzParseval.integrable_norm_sq (f : Comparison.ComplexTest) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => ‖f x‖ ^ 2) MeasureTheory.volume

A Schwartz function has a finite squared L² norm.

theorem NavierStokesR3.SchwartzParseval.integrable_norm_sq_fourier (f : Comparison.ComplexTest) : MeasureTheory.Integrable (fun (ξ : ProblemStatement.Space) => ‖FourierTransform.fourier (⇑f) ξ‖ ^ 2) MeasureTheory.volume

The Fourier transform of a Schwartz function has a finite squared L² norm.

theorem NavierStokesR3.SchwartzParseval.integral_norm_sq_fourier (f : Comparison.ComplexTest) : ∫ (ξ : ProblemStatement.Space), ‖FourierTransform.fourier (⇑f) ξ‖ ^ 2 = ∫ (x : ProblemStatement.Space), ‖f x‖ ^ 2

Parseval's identity for the real squared L² norm of a Schwartz function.

theorem NavierStokesR3.SchwartzParseval.integral_norm_sq_fourierInv (f : Comparison.ComplexTest) : ∫ (ξ : ProblemStatement.Space), ‖(EulerSobolev.schwartzFourier f) (-ξ)‖ ^ 2 = ∫ (x : ProblemStatement.Space), ‖f x‖ ^ 2

Parseval for the inverse Fourier transform of a Schwartz function.