The Fourier integral bundled with Schwartz regularity. Keeping the underlying function explicit lets Sobolev norms expose their formula without exposing the analytic proofs of Fourier inversion and rapid decay.

noncomputable def EulerSobolev.schwartzFourier {V : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (f : SchwartzMap V E) : SchwartzMap V E

The ordinary Fourier integral with its Schwartz smoothness and decay proofs.

Equations

• EulerSobolev.schwartzFourier f = { toFun := FourierTransform.fourier ⇑f, smooth' := ⋯, decay' := ⋯ }

theorem EulerSobolev.schwartzFourier_apply {V : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (f : SchwartzMap V E) (x : V) : (schwartzFourier f) x = FourierTransform.fourier (⇑f) x

The bundled Schwartz transform has exactly the ordinary Fourier integral as its values.

noncomputable def EulerSobolev.schwartzFourierCLM {V : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : SchwartzMap V E →L[ℂ] SchwartzMap V E

The ordinary Fourier integral as a continuous linear map on Schwartz functions.

Equations

• EulerSobolev.schwartzFourierCLM = { toFun := EulerSobolev.schwartzFourier, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }