Ordered derivatives of Sobolev distributions

Each distributional spatial derivative lowers the Bessel order by one. The ordered form supplies the Fourier-integrability threshold for the classical positive-time representative.

theorem CKN.Leray.regularised_orderedLineDeriv_memSobolev (D : TemperedDistribution Foundation.Parabolic.L2Vec3 ComplexVec3) (s : ℝ) (hD : TemperedDistribution.MemSobolev s 2 D) (α : List Foundation.Parabolic.L2Vec3) : TemperedDistribution.MemSobolev (s - ↑α.length) 2 (List.foldl (fun (F : TemperedDistribution Foundation.Parabolic.L2Vec3 ComplexVec3) (m : Foundation.Parabolic.L2Vec3) => LineDeriv.lineDerivOp m F) D α)

An ordered finite list of spatial directions lowers the Sobolev order by the number of directional derivatives.

theorem CKN.Leray.regularisedBesselEven_orderedLineDeriv_L2 (k : ℕ) (v : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) (α : List Foundation.Parabolic.L2Vec3) (hα : α.length ≤ 2 * k) : ∃ (g : ↥ComplexVectorL2), List.foldl (fun (D : TemperedDistribution Foundation.Parabolic.L2Vec3 ComplexVec3) (m : Foundation.Parabolic.L2Vec3) => LineDeriv.lineDerivOp m D) (↑v) α = MeasureTheory.Lp.toTemperedDistribution g

Every ordered derivative through the Bessel order is represented by a spatial L² field as a tempered distribution.