High-order tensor frequency realization for pressure

The tensor Bessel realization is an inverse polynomial Fourier multiplier. The double-Riesz pressure map can therefore use the same high-order frequency lift as the regularized tensor.

noncomputable def ESS.lpsTensorBesselSymbol (k : ℕ) (p : CKN.Foundation.Parabolic.L2Vec3 × CKN.Leray.ComplexTensor3) : CKN.Leray.ComplexTensor3

The Bessel multiplier of order 2 * k acting on a complex tensor.

Equations

• ESS.lpsTensorBesselSymbol k p = ↑((1 + ‖p.1‖ ^ 2) ^ (-↑(2 * k) / 2)) • p.2

theorem ESS.lps_tensorBessel_fourier_ae (k : ℕ) (W : BesselPotentialSpace CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexTensor3 (↑(2 * k)) 2) : ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexTensor3) ((CKN.Leray.regularisedTensorBesselSobolevToL2 ↑(2 * k) ⋯) W)) =ᵐ[MeasureTheory.volume] fun (ξ : CKN.Foundation.Parabolic.L2Vec3) => ↑((1 + ‖ξ‖ ^ 2) ^ (-↑(2 * k) / 2)) • ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ CKN.Foundation.Parabolic.L2Vec3 CKN.Leray.ComplexTensor3) W.toLp) ξ

The tensor Bessel embedding has the inverse Bessel weight in Fourier coordinates at every even order (prop:lps-smoothing).

noncomputable def ESS.lpsRegR12RealCurvePath (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (ha : CKN.IsInJ a) (T : ℝ) : C(↑(CKN.Leray.RegularizedMildTimeInterval T), ↥CKN.Leray.RealVectorL2)

The clamped physical real velocity path associated with a regularized solution on a finite interval.

Equations

• ESS.lpsRegR12RealCurvePath ρ ε hε a ha T = { toFun := fun (t : ↑(CKN.Leray.RegularizedMildTimeInterval T)) => CKN.Leray.regR12Curve ρ ε hε a ha ↑t, continuous_toFun := ⋯ }

noncomputable def ESS.lpsRegR12HighTensorFreq (ρ : 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 : ℝ) : ↥CKN.Leray.ComplexTensorL2

The high-Bessel Fourier tensor frequency trajectory.

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.lps_regR12HighTensorFreq_continuous (ρ : 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)) : Continuous (lpsRegR12HighTensorFreq ρ ε hε n T hT v)

The high-Bessel tensor frequency path is continuous.

theorem ESS.lps_regR12Pressure_fourier_high_ae (ρ : 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) : ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ CKN.Foundation.Parabolic.L2Vec3 ℂ) (CKN.Leray.pressureL2Operator (CKN.Leray.complexifyTensorL2 (CKN.Leray.regularizedMildTensor ρ ε hε (CKN.Leray.regR12Curve ρ ε hε a ha t))))) =ᵐ[MeasureTheory.volume] fun (ξ : CKN.Foundation.Parabolic.L2Vec3) => ↑((1 + ‖ξ‖ ^ 2) ^ (-↑(2 * (n + 2)) / 2)) • CKN.Leray.pressureApplyFormula ξ (↑↑(lpsRegR12HighTensorFreq ρ ε hε n T hT v t) ξ)

The canonical pressure Fourier field is the double-Riesz image of the high-Bessel tensor lift, with the inverse high-order weight (prop:lps-smoothing).