Decay of Fourier transforms of smooth compactly supported functions

A smooth compactly supported function is a Schwartz function, so its Fourier transform is again a Schwartz function and therefore decays faster than every negative power of ‖v‖. This file records that decay in the elementary form ‖v‖ ^ k * ‖𝓕 f v‖ ≤ C, which is the shape a Fourier transform is used in when it weights a comparison test.

Main declarations

• TauCeti.exists_norm_pow_mul_norm_fourier_le: for every exponent k, the Fourier transform of a smooth compactly supported function on a finite-dimensional real inner product space satisfies ‖v‖ ^ k * ‖𝓕 f v‖ ≤ C for some C > 0.

theorem TauCeti.exists_norm_pow_mul_norm_fourier_le {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup E] [NormedSpace ℂ E] {f : V → E} (hf : ContDiff ℝ (↑⊤) f) (hsupp : HasCompactSupport f) (k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (v : V), ‖v‖ ^ k * ‖FourierTransform.fourier f v‖ ≤ C

The Fourier transform of a smooth compactly supported function decays faster than every power of ‖v‖⁻¹, because it is a Schwartz function.