Kernels of band-limited symbols and Hörmander's condition

Let V be a finite-dimensional real inner product space of dimension n, b an orthonormal basis of V, and 2N > n. Call a Schwartz function σ on V, with values in a complex Hilbert space, adapted to the scale t > 0 with constant A if it vanishes outside closedBall 0 t and its derivatives of order k ≤ N along b are bounded by A t ^ (-k). A smooth symbol m satisfying the Mihlin conditions ‖∂^α m(ξ)‖ ≤ A ‖ξ‖ ^ (-|α|), cut off by a Littlewood–Paley partition of unity to the annulus ‖ξ‖ ~ 2 ^ j, gives such a piece at a scale comparable to 2 ^ j, with constant a fixed multiple of A.

The estimates of SchwartzMap.exists_setIntegral_norm_fourierInv_le and SchwartzMap.exists_integral_norm_fourierInv_le then become scale-invariant bounds on the kernel 𝓕⁻ σ, with constants independent of σ, t and A:

• the tail bound ∫_{‖x‖ > R} ‖𝓕⁻ σ x‖ dx ≤ C A (t R) ^ (n/2 - N);
• the L¹ bound ∫ ‖𝓕⁻ σ x‖ dx ≤ C A, which only needs the derivatives of orders 0 and N;
• the smoothness bound ∫ ‖𝓕⁻ σ (x + h) - 𝓕⁻ σ x‖ dx ≤ C A t ‖h‖. Translating the kernel by h is controlled by the symbol ⟪h, ξ⟫ σ ξ, whose derivatives the Leibniz rule SchwartzMap.iterate_lineDerivOp_smulLeftCLM_clm bounds.

For pieces σ j adapted to the dyadic scales 2 ^ j, j ∈ s, the smoothness bound is the better one when 2 ^ j ‖h‖ ≤ 1 and the tail bound when 2 ^ j ‖h‖ > 1. Summing the better of the two over j (TauCeti.sum_min_zpow_mul_rpow_neg_le) gives Hörmander's condition

∫_{‖x‖ > 2 ‖h‖} ‖K (x - h) - K x‖ dx ≤ C A for K = 𝓕⁻ (∑ j ∈ s, σ j),

with C independent of the finite set s and of h. This is the kernel estimate in the proof of the Mihlin–Hörmander multiplier theorem: the finite partial sums of the Littlewood–Paley pieces of a Mihlin symbol have kernels satisfying Hörmander's condition uniformly in the partial sum.

Main declarations

• SchwartzMap.norm_toLp_two_le_of_support_subset_closedBall: the L² norm of a bounded Schwartz function vanishing outside a ball.
• SchwartzMap.exists_setIntegral_norm_fourierInv_le_of_support_subset: the tail bound.
• SchwartzMap.exists_integral_norm_fourierInv_le_of_support_subset: the L¹ bound.
• SchwartzMap.exists_integral_norm_fourierInv_add_sub_le_of_support_subset: the smoothness bound.
• SchwartzMap.exists_setIntegral_norm_fourierInv_sub_sub_le_of_support_subset: Hörmander's condition for one band-limited piece, the better of the smoothness and tail bounds.
• SchwartzMap.exists_setIntegral_norm_fourierInv_sum_sub_sub_le: Hörmander's condition for dyadic sums.

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.
• L. Hörmander, Estimates for translation invariant operators in Lᵖ spaces, Acta Math. 104 (1960), 93–140.

theorem SchwartzMap.norm_toLp_two_le_of_support_subset_closedBall {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] [NormedAddCommGroup H] [NormedSpace ℝ H] (f : SchwartzMap V H) {t M : ℝ} (ht : 0 ≤ t) (hf : Function.support ⇑f ⊆ Metric.closedBall 0 t) (hfM : ∀ (ξ : V), ‖f ξ‖ ≤ M) : ‖f.toLp 2 MeasureTheory.volume‖ ≤ M * √(MeasureTheory.volume.real (Metric.ball 0 1)) * t ^ (↑(Module.finrank ℝ V) / 2)

A Schwartz function bounded by M and vanishing outside closedBall 0 t has L² norm at most M √|B(0, 1)| t ^ (n/2).

theorem SchwartzMap.exists_setIntegral_norm_fourierInv_le_of_support_subset {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) {t A : ℝ}, 0 < t → 0 ≤ A → Function.support ⇑σ ⊆ Metric.closedBall 0 t → (∀ (i : ι) (ξ : V), ‖((LineDeriv.lineDerivOp (b i))^[N] σ) ξ‖ ≤ A / t ^ N) → ∀ (R : ℝ), 0 < R → ∫ (x : V) in {x : V | R < ‖x‖}, ‖(FourierTransformInv.fourierInv σ) x‖ ≤ C * A * (t * R) ^ (↑(Module.finrank ℝ V) / 2 - ↑N)

The tail of the kernel of a band-limited symbol. Let b be an orthonormal basis of the n-dimensional space V and 2N > n. There is a constant C ≥ 0 such that, whenever a Schwartz function σ vanishes outside closedBall 0 t and its N-th derivatives along b are bounded by A t ^ (-N),

∫_{‖x‖ > R} ‖𝓕⁻ σ x‖ dx ≤ C A (t R) ^ (n/2 - N) for every R > 0.

theorem SchwartzMap.exists_integral_norm_fourierInv_le_of_support_subset {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) {t A : ℝ}, 0 < t → Function.support ⇑σ ⊆ Metric.closedBall 0 t → (∀ (ξ : V), ‖σ ξ‖ ≤ A) → (∀ (i : ι) (ξ : V), ‖((LineDeriv.lineDerivOp (b i))^[N] σ) ξ‖ ≤ A / t ^ N) → ∫ (x : V), ‖(FourierTransformInv.fourierInv σ) x‖ ≤ C * A

The L¹ norm of the kernel of a band-limited symbol. Let b be an orthonormal basis of the n-dimensional space V and 2N > n. There is a constant C ≥ 0 such that, whenever a Schwartz function σ vanishes outside closedBall 0 t, is bounded by A and its N-th derivatives along b are bounded by A t ^ (-N),

∫ ‖𝓕⁻ σ x‖ dx ≤ C A.

theorem SchwartzMap.exists_integral_norm_fourierInv_add_sub_le_of_support_subset {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) {t A : ℝ}, 0 < t → 0 ≤ A → Function.support ⇑σ ⊆ Metric.closedBall 0 t → (∀ k ≤ N, ∀ (i : ι) (ξ : V), ‖((LineDeriv.lineDerivOp (b i))^[k] σ) ξ‖ ≤ A / t ^ k) → ∀ (h : V), ∫ (x : V), ‖(FourierTransformInv.fourierInv σ) (x + h) - (FourierTransformInv.fourierInv σ) x‖ ≤ C * A * (t * ‖h‖)

The smoothness of the kernel of a band-limited symbol. Let b be an orthonormal basis of the n-dimensional space V and 2N > n. There is a constant C ≥ 0 such that, whenever a Schwartz function σ vanishes outside closedBall 0 t and its derivatives of order k ≤ N along b are bounded by A t ^ (-k),

∫ ‖𝓕⁻ σ (x + h) - 𝓕⁻ σ x‖ dx ≤ C A t ‖h‖ for every h.

theorem SchwartzMap.exists_setIntegral_norm_fourierInv_sub_sub_le_of_support_subset {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) {t A : ℝ}, 0 < t → 0 ≤ A → Function.support ⇑σ ⊆ Metric.closedBall 0 t → (∀ k ≤ N, ∀ (i : ι) (ξ : V), ‖((LineDeriv.lineDerivOp (b i))^[k] σ) ξ‖ ≤ A / t ^ k) → ∀ (h : V), ∫ (x : V) in {x : V | 2 * ‖h‖ < ‖x‖}, ‖(FourierTransformInv.fourierInv σ) (x - h) - (FourierTransformInv.fourierInv σ) x‖ ≤ C * A * min (t * ‖h‖) ((t * ‖h‖) ^ (↑(Module.finrank ℝ V) / 2 - ↑N))

Hörmander's condition for the kernel of a band-limited symbol. Let b be an orthonormal basis of the n-dimensional space V and 2N > n. There is a constant C ≥ 0 such that, whenever a Schwartz function σ vanishes outside closedBall 0 t and its derivatives of order k ≤ N along b are bounded by A t ^ (-k),

∫_{‖x‖ > 2 ‖h‖} ‖𝓕⁻ σ (x - h) - 𝓕⁻ σ x‖ dx ≤ C A min (t ‖h‖, (t ‖h‖) ^ (n/2 - N))

for every h: the smoothness bound is the better one when t ‖h‖ ≤ 1, the tail bound when t ‖h‖ > 1.

theorem SchwartzMap.exists_setIntegral_norm_fourierInv_sum_sub_sub_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) (s : Finset ℤ) {A : ℝ}, 0 ≤ A → (∀ j ∈ s, Function.support ⇑(σ j) ⊆ Metric.closedBall 0 (2 ^ j)) → (∀ j ∈ s, ∀ k ≤ N, ∀ (i : ι) (ξ : V), ‖((LineDeriv.lineDerivOp (b i))^[k] (σ j)) ξ‖ ≤ A / (2 ^ j) ^ k) → ∀ (h : V), ∫ (x : V) in {x : V | 2 * ‖h‖ < ‖x‖}, ‖(FourierTransformInv.fourierInv (∑ j ∈ s, σ j)) (x - h) - (FourierTransformInv.fourierInv (∑ j ∈ s, σ j)) x‖ ≤ C * A

Hörmander's condition for dyadic sums of band-limited symbols. Let b be an orthonormal basis of the n-dimensional space V and 2N > n. There is a constant C ≥ 0 with the following property. Let σ j be Schwartz functions, for j in a finite set s ⊆ ℤ, such that σ j vanishes outside closedBall 0 (2 ^ j) and its derivatives of order k ≤ N along b are bounded by A 2 ^ (-j k). Then the kernel K = 𝓕⁻ (∑ j ∈ s, σ j) satisfies

∫_{‖x‖ > 2 ‖h‖} ‖K (x - h) - K x‖ dx ≤ C A for every h.