Ordered Fourier coordinate symbols

A spatial word corresponds to a product of coordinate frequency multipliers. Its growth is bounded by the word length, which is the input for the all-order Bessel-to-classical derivative bridge.

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

Fourier multiplier of an ordered spatial derivative word.

Equations

• ESS.lpsFourierWordSymbol α ξ = (List.map (fun (j : Fin 3) => CKN.Leray.regR12CoordSymbol j ξ) α).prod

theorem ESS.lps_fourierWordSymbol_append (α : List (Fin 3)) (j : Fin 3) (ξ : CKN.Foundation.Parabolic.L2Vec3) : lpsFourierWordSymbol (α ++ [j]) ξ = CKN.Leray.regR12CoordSymbol j ξ * lpsFourierWordSymbol α ξ

Appending one derivative multiplies by its coordinate symbol.

theorem ESS.lps_fourierWordSymbol_norm_le (α : List (Fin 3)) (ξ : CKN.Foundation.Parabolic.L2Vec3) : ‖lpsFourierWordSymbol α ξ‖ ≤ (2 * Real.pi) ^ α.length * ‖ξ‖ ^ α.length

An ordered word of length r has at most polynomial Fourier growth of order r (prop:lps-smoothing).

theorem ESS.lps_power_le_bessel_even (r k : ℕ) (hr : r ≤ 2 * k) (x : ℝ) (hx : 0 ≤ x) : x ^ r ≤ (1 + x ^ 2) ^ k

A Bessel weight of order 2k absorbs a polynomial of degree at most 2k (prop:lps-smoothing).

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

A Fourier word of length at most 2k is bounded by the order-2k Bessel weight (prop:lps-smoothing).