Smooth spatial slices of the canonical regularized pressure

Every finite Bessel order controls the corresponding finite number of Fourier moments of the canonical pressure. The pointwise high-order models agree with the canonical pressure at positive times.

theorem ESS.lps_dampedPressureField_moment_integrable (n r : ℕ) (hr : r ≤ 2 * (n + 1)) (G : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : MeasureTheory.Integrable (fun (ξ : CKN.Foundation.Parabolic.L2Vec3) => ‖ξ‖ ^ r * ‖lpsDampedFourierWordSymbol n [] ξ • ↑((1 + ‖ξ‖ ^ 2) ^ (-2)) • ↑↑G ξ‖) MeasureTheory.volume

A damped scalar pressure frequency field has every Fourier moment up to its available Bessel order (prop:lps-smoothing).

theorem ESS.lps_regR12PressureHighModel_slice_contDiff (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (n m : ℕ) (hm : m ≤ 2 * (n + 1)) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(CKN.Leray.RegularizedMildTimeInterval T), BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3 (↑(2 * (n + 2))) 2)) (t : ℝ) : ContDiff ℝ ↑m fun (x : CKN.Foundation.Parabolic.Vec3) => lpsRegR12PressureHighModel ρ ε hε n T hT v (x, t)

A pressure model at Bessel order 2(n+2) is spatially C^m whenever m ≤ 2(n+1) (prop:lps-smoothing).

theorem ESS.lps_regR12Pressure_slice_contDiff (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (t : ℝ) (ht : 0 < t) : ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.forcedQuadPressure ρ ε hε (CKN.Leray.regR12Curve ρ ε hε a ha) (x, t)

The canonical pressure of the regularized velocity is spatially smooth at every positive time (prop:lps-smoothing).

theorem ESS.lps_regR12Pressure_all_word_memLp_slice (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (t : ℝ) (ht : 0 < t) (α : List (Fin 3)) : MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.forcedQuadPressure ρ ε hε (CKN.Leray.regR12Curve ρ ε hε a ha) (x, t)) 2 MeasureTheory.volume

Every classical ordered spatial derivative of the canonical regularized pressure belongs to spatial L² on a positive-time slice (prop:lps-smoothing).