Littlewood–Paley pieces of a Mihlin symbol

Let φ : E → ℝ be a smooth bump function on a finite-dimensional real normed space, and let ψⱼ ξ = φ (2^{-j} ξ) - φ (2^{1-j} ξ) be the dyadic Littlewood–Paley cutoffs built from it (ContDiffBump.littlewoodPaley), which form a smooth partition of unity of E \ {0} with each ψⱼ supported in the annulus 2^{j-1} φ.rIn ≤ ‖ξ‖ ≤ 2^j φ.rOut.

Cutting a symbol m that is smooth away from the origin by this partition gives the Schwartz functions ψⱼ • m, which sum to m pointwise on E \ {0}. If m satisfies Mihlin's condition of order N with constant A,

‖D^k m ξ‖ ≤ A ‖ξ‖^{-k} for k ≤ N and ξ ≠ 0,

then each piece is supported in closedBall 0 (2^j φ.rOut) and its derivatives satisfy the scale-invariant bounds ‖D^k (ψⱼ • m) ξ‖ ≤ C A 2^{-jk} for k ≤ N, with C depending only on φ and N, uniformly over the normed real codomain of m. On the annulus carrying ψⱼ, the Leibniz rule pairs the factor 2^{-ji} from i derivatives of ψⱼ with the factor ‖ξ‖^{-(k-i)} ≈ 2^{-j(k-i)} from the remaining derivatives of m.

This is the decomposition at the start of the proof of the Mihlin–Hörmander multiplier theorem: each piece is band-limited at scale 2^j with derivative bounds independent of j, which is the input to the kernel estimates that establish Hörmander's condition for the kernel of the multiplier.

The inhomogeneous partition ψ₀ = φ, ψⱼ = φ (2^{-j} ·) - φ (2^{1-j} ·) (j ≥ 1) of all of E (ContDiffBump.inhomogeneousLittlewoodPaley) instead reconstructs every Schwartz function: the partial sums of the Fourier multipliers 𝓕⁻ (ψⱼ • 𝓕 f) are the low-pass truncations 𝓕⁻ (φ (2^{-N} ·) • 𝓕 f), and these converge to f in the Schwartz topology.

Main declarations

• ContDiffBump.littlewoodPaleyPiece: the Schwartz function ψⱼ • m.
• ContDiffBump.hasSum_littlewoodPaleyPiece: the pieces sum to m away from the origin.
• ContDiffBump.exists_norm_iteratedFDeriv_littlewoodPaleyPiece_le: the scale-invariant derivative bounds for the pieces of a symbol satisfying Mihlin's condition.
• SchwartzMap.exists_eqOn_annulus_of_contDiffOn: a symbol smooth away from the origin agrees with a Schwartz function on every annulus 1 ≤ ‖ξ‖ ≤ θ.
• SchwartzMap.sum_fourierMultiplierCLM_inhomogeneousLittlewoodPaley_range: the partial sums of the inhomogeneous Littlewood–Paley multipliers are the low-pass truncations.
• SchwartzMap.tendsto_sum_fourierMultiplierCLM_inhomogeneousLittlewoodPaley: Littlewood–Paley reconstruction of a Schwartz function from the inhomogeneous partition.

References

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

noncomputable def ContDiffBump.littlewoodPaleyPiece {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] (φ : ContDiffBump 0) {m : E → F} (hm : ContDiffOn ℝ (↑⊤) m {0}ᶜ) (j : ℤ) : SchwartzMap E F

The Littlewood–Paley piece ψⱼ • m of a function m smooth away from the origin, as a Schwartz function. It is supported in closedBall 0 (2^j φ.rOut), and the pieces sum to m on E \ {0}.

@[simp]

theorem ContDiffBump.littlewoodPaleyPiece_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] (φ : ContDiffBump 0) {m : E → F} (hm : ContDiffOn ℝ (↑⊤) m {0}ᶜ) (j : ℤ) (ξ : E) : (φ.littlewoodPaleyPiece hm j) ξ = φ.littlewoodPaley j ξ • m ξ

The values of the piece ψⱼ • m.

theorem ContDiffBump.coe_littlewoodPaleyPiece {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] (φ : ContDiffBump 0) {m : E → F} (hm : ContDiffOn ℝ (↑⊤) m {0}ᶜ) (j : ℤ) : ⇑(φ.littlewoodPaleyPiece hm j) = fun (ξ : E) => φ.littlewoodPaley j ξ • m ξ

The piece ψⱼ • m, as a function.

theorem ContDiffBump.tsupport_littlewoodPaleyPiece_subset {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] (φ : ContDiffBump 0) {m : E → F} (hm : ContDiffOn ℝ (↑⊤) m {0}ᶜ) (j : ℤ) : tsupport ⇑(φ.littlewoodPaleyPiece hm j) ⊆ {ξ : E | 2 ^ (j - 1) * φ.rIn ≤ ‖ξ‖ ∧ ‖ξ‖ ≤ 2 ^ j * φ.rOut}

The piece ψⱼ • m is supported in the closed annulus 2^{j-1} φ.rIn ≤ ‖ξ‖ ≤ 2^j φ.rOut.

theorem ContDiffBump.sum_littlewoodPaleyPiece_Ioc {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] (φ : ContDiffBump 0) {m : E → F} (hm : ContDiffOn ℝ (↑⊤) m {0}ᶜ) {a b : ℤ} (hab : a ≤ b) (ξ : E) : ∑ j ∈ Finset.Ioc a b, (φ.littlewoodPaleyPiece hm j) ξ = (↑φ ((2 ^ b)⁻¹ • ξ) - ↑φ ((2 ^ a)⁻¹ • ξ)) • m ξ

The partial sums of the pieces are the truncations ∑_{a < j ≤ b} ψⱼ • m = (φ (2^{-b} ·) - φ (2^{-a} ·)) • m.

theorem ContDiffBump.hasSum_littlewoodPaleyPiece {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] (φ : ContDiffBump 0) {m : E → F} (hm : ContDiffOn ℝ (↑⊤) m {0}ᶜ) {ξ : E} (hξ : ξ ≠ 0) : HasSum (fun (j : ℤ) => (φ.littlewoodPaleyPiece hm j) ξ) (m ξ)

The Littlewood–Paley pieces of m sum to m away from the origin.

theorem ContDiffBump.exists_norm_iteratedFDeriv_littlewoodPaleyPiece_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (φ : ContDiffBump 0) (N : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : E → F} (hm : ContDiffOn ℝ (↑⊤) m {0}ᶜ) {A : ℝ}, 0 ≤ A → (∀ k ≤ N, ∀ (ξ : E), ξ ≠ 0 → ‖iteratedFDeriv ℝ k m ξ‖ ≤ A / ‖ξ‖ ^ k) → ∀ (j : ℤ), ∀ k ≤ N, ∀ (ξ : E), ‖iteratedFDeriv ℝ k (⇑(φ.littlewoodPaleyPiece hm j)) ξ‖ ≤ C * A / (2 ^ j) ^ k

Littlewood–Paley pieces of a Mihlin symbol. Let m be smooth on E \ {0} and satisfy Mihlin's condition of order N with constant A ≥ 0: ‖D^k m ξ‖ ≤ A / ‖ξ‖^k for k ≤ N and ξ ≠ 0. Then every Littlewood–Paley piece ψⱼ • m, which is supported in closedBall 0 (2^j φ.rOut), satisfies ‖D^k (ψⱼ • m) ξ‖ ≤ C A / 2^{jk} for k ≤ N, where C depends only on φ and N, uniformly over the normed real codomain of m.

theorem SchwartzMap.exists_eqOn_annulus_of_contDiffOn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : E → F} (hm : ContDiffOn ℝ (↑⊤) m {0}ᶜ) (θ : ℝ) : ∃ (σ : SchwartzMap E F), Set.EqOn (⇑σ) m {ξ : E | 1 ≤ ‖ξ‖ ∧ ‖ξ‖ ≤ θ}

A function m smooth away from the origin agrees on the annulus 1 ≤ ‖ξ‖ ≤ θ with a Schwartz function, namely a finite sum of its Littlewood–Paley pieces.

theorem SchwartzMap.sum_fourierMultiplierCLM_inhomogeneousLittlewoodPaley_range {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] (φ : ContDiffBump 0) (N : ℕ) : (∑ j ∈ Finset.range (N + 1), fourierMultiplierCLM F fun (ξ : E) => ↑(φ.inhomogeneousLittlewoodPaley j ξ)) = fourierMultiplierCLM F fun (ξ : E) => ↑(↑φ ((2 ^ N)⁻¹ • ξ))

The partial sums of the Fourier multipliers by the inhomogeneous Littlewood–Paley pieces are the low-pass truncations: ∑_{j ≤ N} 𝓕⁻ (ψⱼ • 𝓕 ·) = 𝓕⁻ (φ (2^{-N} ·) • 𝓕 ·).

theorem SchwartzMap.tendsto_sum_fourierMultiplierCLM_inhomogeneousLittlewoodPaley {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (φ : ContDiffBump 0) (f : SchwartzMap E F) : Filter.Tendsto (fun (N : ℕ) => ∑ j ∈ Finset.range N, (fourierMultiplierCLM F fun (ξ : E) => ↑(φ.inhomogeneousLittlewoodPaley j ξ)) f) Filter.atTop (nhds f)

Littlewood–Paley reconstruction of a Schwartz function. The partial sums of the Littlewood–Paley pieces 𝓕⁻ (ψⱼ • 𝓕 f) of a Schwartz function f converge to f in the Schwartz topology.