theorem FourierL1BoundedC0.fourier_norm_le_L1_norm {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : V → E) (w : V) : ‖FourierTransform.fourier f w‖ ≤ ∫ (v : V), ‖f v‖

The Fourier transform is bounded L¹ → L∞: for any integrable function f, the pointwise norm of 𝓕 f is dominated by the L¹ norm of f.

theorem FourierL1BoundedC0.fourier_tendsto_zero_at_infty {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : V → E) : Filter.Tendsto (FourierTransform.fourier f) (Filter.cocompact V) (nhds 0)

Riemann–Lebesgue lemma: the Fourier transform of an L¹ function tends to zero at infinity, so 𝓕 : L¹(V) → C₀(V) is well-defined.