Weighted Plancherel and L¹ bounds for inverse Fourier transforms

Let V be a finite-dimensional real inner product space of dimension n and σ a Schwartz function on V with values in a complex Hilbert space. Differentiating σ along m multiplies its inverse Fourier transform by -2πi ⟪x, m⟫, so Plancherel's theorem gives the weighted Plancherel identity

(2π) ^ (2N) ∫ ⟪x, m⟫ ^ (2N) ‖𝓕⁻ σ x‖² dx = ‖∂_m^N σ‖²_{L²}.

Summing it along an orthonormal basis b controls ∫ ‖x‖ ^ (2N) ‖𝓕⁻ σ x‖². When 2N > n, the weight ‖x‖ ^ (-2N) is integrable away from the origin, and the Cauchy–Schwarz inequality turns the weighted L² bound into an L¹ bound on the tail:

∫_{‖x‖ > R} ‖𝓕⁻ σ x‖ dx ≤ C R ^ (n/2 - N) (∑ᵢ ‖∂_{bᵢ}^N σ‖²_{L²}) ^ (1/2).

On the ball ‖x‖ ≤ R, Cauchy–Schwarz and Plancherel bound the integral by C R ^ (n/2) ‖σ‖_{L²}. Together these bound the L¹ norm of the kernel 𝓕⁻ σ by the L² norms of σ and of its derivatives of order N > n/2. This is a quantitative form, for Schwartz functions, of Bernstein's theorem on absolutely convergent Fourier integrals.

These are the estimates on the kernel of a single dyadic piece in the proof of the Mihlin–Hörmander multiplier theorem. If the symbol σ is supported where ‖ξ‖ ~ 2ʲ, its kernel 𝓕⁻ σ is controlled by taking R = 2⁻ʲ. The translation estimate ∫ ‖𝓕⁻ σ (x + h) - 𝓕⁻ σ x‖ ≤ 2π ∫ ‖𝓕⁻ (⟪·, h⟫ σ)‖ reduces the smoothness of the kernel to the same L¹ bound for the symbol ⟪ξ, h⟫ σ(ξ).

Main declarations

• SchwartzMap.integral_inner_pow_mul_norm_fourierInv_sq: the weighted Plancherel identity.
• SchwartzMap.integral_norm_pow_mul_norm_fourierInv_sq_le: its consequence for the weight ‖x‖ ^ (2N).
• SchwartzMap.setIntegral_closedBall_norm_fourierInv_le: the L¹ bound on ‖x‖ ≤ R.
• SchwartzMap.exists_setIntegral_norm_fourierInv_le: the L¹ bound on {‖x‖ > R}.
• SchwartzMap.exists_integral_norm_fourierInv_le: the L¹ bound on V.
• SchwartzMap.integral_norm_fourierInv_add_sub_le: the translation estimate.

References

• L. Grafakos, Classical Fourier Analysis, 3rd ed., Section 6.2 (proof of Theorem 6.2.7).
• E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Chapter IV, §3.

theorem SchwartzMap.integrable_inner_pow_mul_norm_fourierInv_sq {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [NormedSpace ℂ H] (σ : SchwartzMap V H) (m : V) (N : ℕ) : MeasureTheory.Integrable (fun (x : V) => inner ℝ x m ^ (2 * N) * ‖(FourierTransformInv.fourierInv σ) x‖ ^ 2) MeasureTheory.volume

For a Schwartz function σ, the function ⟪x, m⟫ ^ (2N) ‖𝓕⁻ σ x‖² is integrable.

theorem SchwartzMap.integral_norm_fourierInv_add_sub_le {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [NormedSpace ℂ H] (σ : SchwartzMap V H) (h : V) : ∫ (x : V), ‖(FourierTransformInv.fourierInv σ) (x + h) - (FourierTransformInv.fourierInv σ) x‖ ≤ 2 * Real.pi * ∫ (x : V), ‖(FourierTransformInv.fourierInv ((smulLeftCLM H fun (x : V) => inner ℝ x h) σ)) x‖

The translation estimate for an inverse Fourier transform: translating 𝓕⁻ σ by h moves it in L¹ by at most 2π times the L¹ norm of the inverse Fourier transform of ξ ↦ ⟪ξ, h⟫ σ ξ.

theorem SchwartzMap.integral_inner_pow_mul_norm_fourierInv_sq {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (σ : SchwartzMap V H) (m : V) (N : ℕ) : (2 * Real.pi) ^ (2 * N) * ∫ (x : V), inner ℝ x m ^ (2 * N) * ‖(FourierTransformInv.fourierInv σ) x‖ ^ 2 = ‖((LineDeriv.lineDerivOp m)^[N] σ).toLp 2 MeasureTheory.volume‖ ^ 2

The weighted Plancherel identity: for a Schwartz function σ,

(2π) ^ (2N) ∫ ⟪x, m⟫ ^ (2N) ‖𝓕⁻ σ x‖² dx = ‖∂_m^N σ‖²_{L²}.

theorem SchwartzMap.integral_norm_pow_mul_norm_fourierInv_sq_le {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_3} [Fintype ι] (σ : SchwartzMap V H) (b : OrthonormalBasis ι ℝ V) {N : ℕ} (hN : N ≠ 0) : (2 * Real.pi) ^ (2 * N) * ∫ (x : V), ‖x‖ ^ (2 * N) * ‖(FourierTransformInv.fourierInv σ) x‖ ^ 2 ≤ ↑(Fintype.card ι) ^ (N - 1) * ∑ i : ι, ‖((LineDeriv.lineDerivOp (b i))^[N] σ).toLp 2 MeasureTheory.volume‖ ^ 2

The weighted Plancherel bound: for a Schwartz function σ, an orthonormal basis b of V indexed by ι, and N ≠ 0,

(2π) ^ (2N) ∫ ‖x‖ ^ (2N) ‖𝓕⁻ σ x‖² dx ≤ (#ι) ^ (N - 1) ∑ᵢ ‖∂_{bᵢ}^N σ‖²_{L²}.

theorem SchwartzMap.setIntegral_closedBall_norm_fourierInv_le {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (σ : SchwartzMap V H) {R : ℝ} (hR : 0 < R) : ∫ (x : V) in Metric.closedBall 0 R, ‖(FourierTransformInv.fourierInv σ) x‖ ≤ √(MeasureTheory.volume.real (Metric.ball 0 1)) * R ^ (↑(Module.finrank ℝ V) / 2) * ‖σ.toLp 2 MeasureTheory.volume‖

The inverse Fourier transform on a ball in L¹, by Cauchy–Schwarz and Plancherel: ∫_{‖x‖ ≤ R} ‖𝓕⁻ σ x‖ dx ≤ √(|B(0, 1)| Rⁿ) ‖σ‖_{L²}.

theorem SchwartzMap.exists_setIntegral_norm_fourierInv_le {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_3} [Fintype ι] (b : OrthonormalBasis ι ℝ V) {N : ℕ} (hN : Module.finrank ℝ V < 2 * N) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (σ : SchwartzMap V H) (R : ℝ), 0 < R → ∫ (x : V) in {x : V | R < ‖x‖}, ‖(FourierTransformInv.fourierInv σ) x‖ ≤ C * R ^ (↑(Module.finrank ℝ V) / 2 - ↑N) * √(∑ i : ι, ‖((LineDeriv.lineDerivOp (b i))^[N] σ).toLp 2 MeasureTheory.volume‖ ^ 2)

The tail of an inverse Fourier transform in L¹. Let b be an orthonormal basis of the n-dimensional space V and 2N > n. There is a constant C ≥ 0 such that for every Schwartz function σ and every R > 0,

∫_{‖x‖ > R} ‖𝓕⁻ σ x‖ dx ≤ C R ^ (n/2 - N) (∑ᵢ ‖∂_{bᵢ}^N σ‖²_{L²}) ^ (1/2).

theorem SchwartzMap.exists_integral_norm_fourierInv_le {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ι : Type u_3} [Fintype ι] (b : OrthonormalBasis ι ℝ V) {N : ℕ} (hN : Module.finrank ℝ V < 2 * N) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (σ : SchwartzMap V H) (R : ℝ), 0 < R → ∫ (x : V), ‖(FourierTransformInv.fourierInv σ) x‖ ≤ C * (R ^ (↑(Module.finrank ℝ V) / 2) * ‖σ.toLp 2 MeasureTheory.volume‖ + R ^ (↑(Module.finrank ℝ V) / 2 - ↑N) * √(∑ i : ι, ‖((LineDeriv.lineDerivOp (b i))^[N] σ).toLp 2 MeasureTheory.volume‖ ^ 2))

An inverse Fourier transform in L¹. Let b be an orthonormal basis of the n-dimensional space V and 2N > n. There is a constant C ≥ 0 such that for every Schwartz function σ and every R > 0,

∫ ‖𝓕⁻ σ x‖ dx ≤ C (R ^ (n/2) ‖σ‖_{L²} + R ^ (n/2 - N) (∑ᵢ ‖∂_{bᵢ}^N σ‖²_{L²}) ^ (1/2)).