Ordered derivatives of the mollified initial state

The mollifier's Fréchet derivative estimate supplies every ordered coordinate derivative required by the finite Hᵏ energy construction.

theorem CKN.Leray.regUniformMollifiedInitial_orderedDerivative_memLp (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (α : List (Fin 3)) (i : Fin 3) : MeasureTheory.MemLp (regularisedOrderedSpatialDerivative α fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedInitial ρ ε hε a x i) 2 MeasureTheory.volume

Every ordered spatial derivative of each component of a mollified Leray datum is square integrable.