The inverse Fourier transform of a convolution

Mathlib's convolution theorem Real.fourier_mul_convolution_eq says that the Fourier transform of the convolution of two integrable functions is the product of their Fourier transforms. Since the inverse Fourier transform is the Fourier transform evaluated at -x (Real.fourierInv_eq_fourier_neg), the same holds for the inverse Fourier transform:

𝓕⁻ (f₁ ⋆ f₂) = 𝓕⁻ f₁ * 𝓕⁻ f₂

(Real.fourierInv_mul_convolution_eq). Read backwards, this writes the pointwise product of two functions with integrable Fourier transforms as the inverse Fourier transform of an integrable function, which is how products are handled in Fourier-side Sobolev estimates.

theorem Real.fourierInv_mul_convolution_eq {E : Type u_1} {R : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedRing R] [NormedSpace ℂ R] [IsScalarTower ℂ R R] [SMulCommClass ℂ R R] [CompleteSpace R] {f₁ f₂ : E → R} (hf₁ : MeasureTheory.Integrable f₁ MeasureTheory.volume) (hf₂ : MeasureTheory.Integrable f₂ MeasureTheory.volume) (x : E) : FourierTransformInv.fourierInv (MeasureTheory.convolution f₁ f₂ (ContinuousLinearMap.mul ℂ R) MeasureTheory.volume) x = FourierTransformInv.fourierInv f₁ x * FourierTransformInv.fourierInv f₂ x

The convolution theorem for the inverse Fourier transform. The inverse Fourier transform of the convolution of two integrable functions is the product of their inverse Fourier transforms.