$|\hat f(\xi)|\le\|f\|_{L^1}$ for integrable $f$ on $\mathbb R^d$

Proved

DbarRegularity.enorm_fourier_le

by Mazecto · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

fourier-analysislp-spaces

Let $d\ge0$ and let $f:\mathbb R^d\to\mathbb C$ be integrable. Then for every $\xi\in\mathbb R^d$ the Fourier integral satisfies

|\hat f(\xi)|=\Big|\int_{\mathbb R^d}e^{-2\pi i\langle x,\xi\rangle}f(x)\,dx\Big|\;\le\;\|f\|_{L^1(\mathbb R^d)} .

This is the uniform bound $\|\hat f\|_\infty\le\|f\|_1$ for the Fourier transform of an integrable function.

Formalization Note. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with Lebesgue measure volume. $\hat f$ is Mathlib's 𝓕 f; the bound is stated in ℝ≥0∞ as ‖𝓕 f ξ‖ₑ ≤ eLpNorm f 1 volume.

Preamble

import Mathlib.Analysis.Fourier.FourierTransform
import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
import Mathlib.Analysis.InnerProductSpace.PiL2

Formal statement

namespace DbarRegularity

open MeasureTheory FourierTransform
open scoped ENNReal

/-- `‖𝓕 f‖_∞ ≤ ‖f‖₁`, pointwise. -/
theorem enorm_fourier_le {d : ℕ} (f : EuclideanSpace ℝ (Fin d) → ℂ) (hf : Integrable f volume)
    (ξ : EuclideanSpace ℝ (Fin d)) : ‖𝓕 f ξ‖ₑ ≤ eLpNorm f 1 volume := by sorry

end DbarRegularity

Source

E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton University Press (1970), Chapter II, § 2.2, p. 29

View graph

∣f^(ξ)∣≤∥f∥L1|\hat f(\xi)|\le\|f\|_{L^1}∣f^​(ξ)∣≤∥f∥L1​ for integrable fff on Rd\mathbb R^dRd

$|\hat f(\xi)|\le\|f\|_{L^1}$ for integrable $f$ on $\mathbb R^d$