Even-order Bessel regularity of the mollified initial field

The all-order derivative bounds for the mollifier give L² representatives for every classical Laplacian iterate, which identify its tempered distributional iterates and yield the complete even-order lift.

noncomputable def CKN.Leray.regularisedSourceDirectionalDerivative (i : Fin 3) (g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The derivative of a source field in the ith standard spatial direction.

Equations

• CKN.Leray.regularisedSourceDirectionalDerivative i g x = (fderiv ℝ g x) (CKN.basisVec i)

noncomputable def CKN.Leray.regularisedSourceVectorLaplacian (g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The componentwise spatial Laplacian of a regularized source vector field.

Equations

• CKN.Leray.regularisedSourceVectorLaplacian g x = ∑ i : Fin 3, CKN.Leray.regularisedSourceDirectionalDerivative i (CKN.Leray.regularisedSourceDirectionalDerivative i g) x

noncomputable def CKN.Leray.regularisedComplexPullback (g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : Foundation.Parabolic.L2Vec3 → ComplexVec3

The pullback of a complex-valued field along the regularized source coordinate map.

Equations

• CKN.Leray.regularisedComplexPullback g x = CKN.Leray.complexifyValue (CKN.Leray.l2Vec3Equiv.symm (g (CKN.Leray.l2Vec3Equiv x)))

theorem CKN.Leray.regUniformMollifiedInitial_bessel_even_lift (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (k : ℕ) : ∃ (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2), regularisedBesselSobolevToL2 ↑(2 * k) ⋯ b = complexifyVectorL2 (MeasureTheory.MemLp.toLp (regUniformSpatialField (regUniformMollifiedInitial ρ ε hε a)) ⋯)

Every even-order Bessel space contains the physical L² class of the smooth mollification of an IsInJ initial field.