Derivatives of Schwartz functions on the Fourier side #

The Fourier transform turns the directional derivative ∂_v on Schwartz space into multiplication by 2πi ⟪ξ, v⟫ (Mathlib's SchwartzMap.fourier_lineDerivOp_eq). This file records the pointwise consequences for second-order operators: with Mathlib's normalization of the Fourier transform,

𝓕 (∂_v ∂_w u) ξ = -(2π)² ⟪ξ, v⟫ ⟪ξ, w⟫ 𝓕 u ξ, and
𝓕 (Δ u) ξ = -(2π)² ‖ξ‖² 𝓕 u ξ.

Since ∑ᵢ ∑ⱼ ⟪ξ, bᵢ⟫² ⟪ξ, bⱼ⟫² = ‖ξ‖⁴ for an orthonormal basis b, Plancherel's theorem turns these into the identity

∑ᵢ ∑ⱼ ‖∂_{bᵢ} ∂_{bⱼ} u‖²_{L²} = ‖Δ u‖²_{L²},

so the Laplacian controls the whole Hessian of u in L². This is the p = 2 case of the Calderón–Zygmund estimate ‖D²u‖_{Lᵖ} ≤ C ‖Δu‖_{Lᵖ}, and the L² input to elliptic regularity for the Laplacian on ℝⁿ.

Fourier multipliers are additive in their symbol and commute with the Laplacian. For every bilinear pairing ∫ M (f x) (h x) of Schwartz functions, the transpose of the multiplier with symbol g is the multiplier with the reflected symbol g (-ξ); in particular a multiplier with an even symbol, such as the Bessel potential ⟨ξ⟩ ^ s, is symmetric.

For the inverse Fourier transform, iterating Mathlib's SchwartzMap.fourierInv_lineDerivOp_eq gives 𝓕⁻ (∂_m^N σ) x = (-2πi ⟪x, m⟫) ^ N 𝓕⁻ σ x, the inverse Fourier transform commutes with postcomposition by a continuous linear map, and Mathlib's norm_fourier_toL2_eq gives Plancherel's theorem ‖𝓕⁻ f‖_{L²} = ‖f‖_{L²}.

For a Schwartz function φ and a nonzero ε, the cut-off exponential y ↦ exp(i ⟪y, ξ⟫) φ(ε y) v is a Schwartz function whose Fourier transform |ε|⁻ⁿ 𝓕 φ (ε⁻¹ (ζ - ξ / 2π)) v concentrates at the frequency ξ / 2π as ε → 0.

Main declarations #

SchwartzMap.fourierMultiplierCLM_add: Fourier multipliers are additive in the symbol.
SchwartzMap.fourierMultiplierCLM_laplacian: Fourier multipliers commute with the Laplacian.
SchwartzMap.fourierInv_apply_eq_fourier_neg: 𝓕⁻ f x = 𝓕 f (-x).
SchwartzMap.fourier_smulLeftCLM_fourierInv_eq: 𝓕 (g • 𝓕⁻ f) = 𝓕⁻ (g (-·) • 𝓕 f).
SchwartzMap.integral_bilin_fourierMultiplierCLM_eq: the transpose of a Fourier multiplier for bilinear pairings has the reflected symbol, ∫ M (T_g f) h = ∫ M f (T_{g (-·)} h).
SchwartzMap.fourier_lineDerivOp_apply: the Fourier transform of a directional derivative.
SchwartzMap.support_fourier_lineDerivOp_subset, SchwartzMap.support_fourier_iteratedLineDerivOp_subset: differentiation does not enlarge the support of the Fourier transform.
SchwartzMap.fourier_lineDerivOp_lineDerivOp_apply: the Fourier transform of a second directional derivative.
SchwartzMap.fourier_laplacian_apply: the Fourier transform of the Laplacian.
SchwartzMap.fourierInv_iterate_lineDerivOp_apply: the inverse Fourier transform of an iterated directional derivative, 𝓕⁻ (∂_m^N σ) x = (-2πi ⟪x, m⟫) ^ N 𝓕⁻ σ x.
SchwartzMap.norm_fourierInv_iterate_lineDerivOp_sq: its consequence for squared norms, ‖𝓕⁻ (∂_m^N σ) x‖² = (2π) ^ (2N) ⟪x, m⟫ ^ (2N) ‖𝓕⁻ σ x‖².
SchwartzMap.exists_seminorm_fourier_le_sum_seminorm: each seminorm ‖ξ‖ ^ k ‖𝓕 g ξ‖ of the Fourier transform is bounded by finitely many Schwartz seminorms of g.
SchwartzMap.fourierInv_postcompCLM_apply: the inverse Fourier transform commutes with postcomposition by a continuous linear map.
SchwartzMap.norm_fourierInv_toL2_eq: Plancherel's theorem for the inverse Fourier transform.
SchwartzMap.norm_toLp_fourierMultiplierCLM_eq: Plancherel's theorem for Fourier multipliers, ‖𝓕⁻ (w • 𝓕 f)‖_{L²} = ‖w • 𝓕 f‖_{L²}.
SchwartzMap.sum_sum_norm_toLp_lineDerivOp_lineDerivOp_sq: the squared L² norms of the second derivatives along an orthonormal basis sum to the squared L² norm of the Laplacian.
SchwartzMap.cutoffExponential: the cut-off exponential y ↦ exp(i ⟪y, ξ⟫) φ(ε y) v.
SchwartzMap.fourier_cutoffExponential: its Fourier transform.

References #

D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Section 9.4.