Prove2Me

Plancherel identity ∥g^∥2=∥g∥2\|\hat g\|_{2}=\|g\|_{2} for g∈L1∩L2(Rd)g\in L^1\cap L^2(\mathbb R^d)

Proved
DbarRegularity.eLpNorm_fourier_two_eq

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

fourier-analysisharmonic-analysislp-spaces

Let d≥0d\ge0 and let g:Rd→Cg:\mathbb R^d\to\mathbb C be integrable and square integrable. Then its Fourier integral g^(ξ)=∫e−2πi⟨x,ξ⟩g(x) dx\hat g(\xi)=\int e^{-2\pi i\langle x,\xi\rangle}g(x)\,dx satisfies

∥g^∥L2(Rd)=∥g∥L2(Rd).\|\hat g\|_{L^2(\mathbb R^d)}=\|g\|_{L^2(\mathbb R^d)} .

This is Plancherel's identity for the classical Fourier integral on L1∩L2L^1\cap L^2.

Formalization Note. Rd\mathbb R^d is EuclideanSpace ℝ (Fin d) with Lebesgue measure volume. g^\hat g is Mathlib's Fourier integral 𝓕 g, and both norms are eLpNorm · 2 volume in ℝ≥0∞.

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

/-- Plancherel on `L¹ ∩ L²` for the Fourier integral. -/
theorem eLpNorm_fourier_two_eq {d : ℕ} (g : EuclideanSpace ℝ (Fin d) → ℂ) (hg1 : Integrable g volume)
    (hg2 : MemLp g 2 volume) : eLpNorm (𝓕 g) 2 volume = eLpNorm g 2 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