High-order Fourier models for the regularized pressure

The double-Riesz image of a high-Bessel tensor lift represents the canonical regularized pressure on each nonnegative-time slice.

noncomputable def ESS.lpsRegR12PressureHighFreq (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (n : ℕ) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(CKN.Leray.RegularizedMildTimeInterval T), BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3 (↑(2 * (n + 2))) 2)) (t : ℝ) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The undamped scalar pressure frequency field of a high tensor lift.

Equations

• ESS.lpsRegR12PressureHighFreq ρ ε hε n T hT v t = CKN.Leray.pressureFourierMultiplier (ESS.lpsRegR12HighTensorFreq ρ ε hε n T hT v t)

noncomputable def ESS.lpsRegR12PressureHighModel (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (n : ℕ) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(CKN.Leray.RegularizedMildTimeInterval T), BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3 (↑(2 * (n + 2))) 2)) : CKN.Foundation.Parabolic.ParabolicPoint → ℝ

The inverse Fourier field associated with a high-order pressure frequency path.

Equations

• ESS.lpsRegR12PressureHighModel ρ ε hε n T hT v = CKN.Leray.regR12SpaceTimeField Complex.reCLM (ESS.lpsDampedFourierWordSymbol n []) (ESS.lpsRegR12PressureHighFreq ρ ε hε n T hT v)

theorem ESS.lps_regR12PressureHighModel_ae_eq (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (n : ℕ) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(CKN.Leray.RegularizedMildTimeInterval T), BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3 (↑(2 * (n + 2))) 2)) (hv : ∀ (t : ↑(CKN.Leray.RegularizedMildTimeInterval T)), (CKN.Leray.regularisedBesselSobolevToL2CLM ↑(2 * (n + 2)) ⋯) (v t) = CKN.Leray.complexifyVectorL2 (CKN.Leray.regR12Curve ρ ε hε a ha ↑t)) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : (fun (x : CKN.Foundation.Parabolic.Vec3) => lpsRegR12PressureHighModel ρ ε hε n T hT v (x, t)) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.forcedQuadPressure ρ ε hε (CKN.Leray.regR12Curve ρ ε hε a ha) (x, t)

On each finite-time slice, the high-order pressure model agrees almost everywhere with the canonical pressure (prop:lps-smoothing).

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

The canonical regularized pressure has a continuous spatial slice at every positive time.

theorem ESS.lps_regR12PressureHighModel_eq (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (n : ℕ) (T : ℝ) (hT : 0 ≤ T) (v : C(↑(CKN.Leray.RegularizedMildTimeInterval T), BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexVec3 (↑(2 * (n + 2))) 2)) (hv : ∀ (t : ↑(CKN.Leray.RegularizedMildTimeInterval T)), (CKN.Leray.regularisedBesselSobolevToL2CLM ↑(2 * (n + 2)) ⋯) (v t) = CKN.Leray.complexifyVectorL2 (CKN.Leray.regR12Curve ρ ε hε a ha ↑t)) (t : ℝ) (ht : t ∈ Set.Icc 0 T) (htpos : 0 < t) : (fun (x : CKN.Foundation.Parabolic.Vec3) => lpsRegR12PressureHighModel ρ ε hε n T hT v (x, t)) = fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.forcedQuadPressure ρ ε hε (CKN.Leray.regR12Curve ρ ε hε a ha) (x, t)

A high-Bessel pressure model equals the canonical pressure pointwise on every positive-time slice (prop:lps-smoothing).