Damped high-order Fourier multipliers

A higher Bessel lift can be fed into the order-four inverse Fourier field after the excess Bessel weight is moved into the multiplier.

noncomputable def ESS.lpsDampedFourierWordSymbol (n : ℕ) (α : List (Fin 3)) (ξ : CKN.Foundation.Parabolic.L2Vec3) : ℂ

A coordinate word multiplier damped by an additional Bessel weight of order 2n.

Equations

• ESS.lpsDampedFourierWordSymbol n α ξ = ESS.lpsFourierWordSymbol α ξ * ↑((1 + ‖ξ‖ ^ 2) ^ (-↑n))

theorem ESS.lps_damped_power_bound (n r : ℕ) (hr : r ≤ 2 * (n + 1)) (x : ℝ) (hx : 0 ≤ x) : x ^ r * (1 + x ^ 2) ^ (-↑n) ≤ 1 + x ^ 2

Damping by an even Bessel power leaves at most quadratic growth for every polynomial power below the available order (prop:lps-smoothing).

theorem ESS.lps_dampedFourierWordSymbol_norm_le (n : ℕ) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) (ξ : CKN.Foundation.Parabolic.L2Vec3) : ‖lpsDampedFourierWordSymbol n α ξ‖ ≤ (2 * Real.pi) ^ α.length * (1 + ‖ξ‖ ^ 2)

The damped word multiplier has at most quadratic growth when its word length fits under the higher Bessel order (prop:lps-smoothing).

theorem ESS.lps_dampedFourierWordSymbol_first_moment_le (n : ℕ) (α : List (Fin 3)) (hα : α.length + 1 ≤ 2 * (n + 1)) (ξ : CKN.Foundation.Parabolic.L2Vec3) : ‖ξ‖ * ‖lpsDampedFourierWordSymbol n α ξ‖ ≤ (2 * Real.pi) ^ α.length * (1 + ‖ξ‖ ^ 2)

One additional coordinate derivative still has quadratic growth when the higher Bessel order has one spare degree (prop:lps-smoothing).

theorem ESS.lps_dampedFourierWordSymbol_weighted_norm_le (n : ℕ) (α : List (Fin 3)) (hα : α.length ≤ 2 * (n + 1)) (ξ : CKN.Foundation.Parabolic.L2Vec3) : ‖lpsDampedFourierWordSymbol n α ξ * ↑((1 + ‖ξ‖ ^ 2) ^ (-2))‖ ≤ (2 * Real.pi) ^ α.length

After multiplication by the order-four inverse Bessel weight, the damped coordinate multiplier is bounded at every frequency (prop:lps-smoothing).