Commit 2026-03-10 22:48 f84529f2

View on Github →

feat(Analysis/Distribution): Fourier multiplier (#34099) We define Fourier multiplier with temperate growth functions acting on Schwartz functions as well as tempered distributions. We prove that the directional derivative and the Laplacian can be represented as Fourier multiplier.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Distribution/FourierMultiplier.lean

added def SchwartzMap.fourierMultiplierCLM

added theorem SchwartzMap.fourierMultiplierCLM_apply

added theorem SchwartzMap.fourierMultiplierCLM_compL_fourierMultiplierCLM

added theorem SchwartzMap.fourierMultiplierCLM_const

added theorem SchwartzMap.fourierMultiplierCLM_fourierMultiplierCLM_apply

added theorem SchwartzMap.fourierMultiplierCLM_ofReal

added theorem SchwartzMap.fourierMultiplierCLM_smul

added theorem SchwartzMap.fourierMultiplierCLM_sum

added theorem SchwartzMap.laplacian_eq_fourierMultiplierCLM

added theorem SchwartzMap.lineDeriv_eq_fourierMultiplierCLM

added def TemperedDistribution.fourierMultiplierCLM

added theorem TemperedDistribution.fourierMultiplierCLM_apply

added theorem TemperedDistribution.fourierMultiplierCLM_apply_apply

added theorem TemperedDistribution.fourierMultiplierCLM_compL_fourierMultiplierCLM

added theorem TemperedDistribution.fourierMultiplierCLM_const

added theorem TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply

added theorem TemperedDistribution.fourierMultiplierCLM_smul

added theorem TemperedDistribution.fourierMultiplierCLM_sum

added theorem TemperedDistribution.fourierMultiplierCLM_toTemperedDistributionCLM_eq

added theorem TemperedDistribution.laplacian_eq_fourierMultiplierCLM

added theorem TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM