Ordered pressure multipliers in frequency space #
The double-Riesz pressure symbol has norm at most one. A high Bessel weight therefore absorbs every finite ordered spatial derivative of the pressure frequency field.
noncomputable def
ESS.lpsPressureDampedFrequency
(n : ℕ)
(α : List (Fin 3))
(G : ↥CKN.Leray.ComplexTensorL2)
(ξ : CKN.Foundation.Parabolic.L2Vec3)
:
An ordered pressure Fourier field generated by a high-Bessel tensor frequency field.
Equations
- ESS.lpsPressureDampedFrequency n α G ξ = ESS.lpsDampedFourierWordSymbol n α ξ * ↑((1 + ‖ξ‖ ^ 2) ^ (-2)) * CKN.Leray.pressureApplyFormula ξ (↑↑G ξ)
Instances For
theorem
ESS.lps_pressureDampedFrequency_aestronglyMeasurable
(n : ℕ)
(α : List (Fin 3))
(G : ↥CKN.Leray.ComplexTensorL2)
:
The ordered pressure frequency field is strongly measurable.
theorem
ESS.lps_pressureDampedFrequency_memLp
(n : ℕ)
(α : List (Fin 3))
(hα : α.length ≤ 2 * (n + 1))
(G : ↥CKN.Leray.ComplexTensorL2)
:
A Bessel lift of order 2(n+2) controls every pressure word of
length at most 2(n+1) in frequency L²
(prop:lps-smoothing).