Continuity of the Fourier transform of an integrable function

On a finite-dimensional real inner-product space, the Fourier transform 𝓕 F of an integrable F is continuous, and so is the inverse transform 𝓕⁻ F = 𝓕 F ∘ (-·). These are Mathlib's VectorFourier.fourierIntegral_continuous specialized to the inner-product pairing, packaged so that consumers do not repeat the innerₗ/continuous_inner bridge at every call site.

Nothing here is specific to positive-definite functions or to the Bochner roadmap; the file sits outside TauCeti/Analysis/Bochner/ so that it can be used by any Fourier-analysis development.

Main declarations

• TauCeti.continuous_fourier_of_integrable: 𝓕 F is continuous for integrable F.
• TauCeti.continuous_fourierInv_of_integrable: 𝓕⁻ F is continuous for integrable F.

theorem TauCeti.continuous_fourier_of_integrable {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : V → ℂ} (hint : MeasureTheory.Integrable F MeasureTheory.volume) : Continuous (FourierTransform.fourier F)

The Fourier transform of an integrable function is continuous. This is Mathlib's VectorFourier.fourierIntegral_continuous specialized to the inner-product pairing.

theorem TauCeti.continuous_fourierInv_of_integrable {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : V → ℂ} (hint : MeasureTheory.Integrable F MeasureTheory.volume) : Continuous (FourierTransformInv.fourierInv F)

The inverse Fourier transform of an integrable function is continuous: it is the Fourier transform precomposed with negation.