Ordered derivative bound for Schwartz mollification

Each finite ordered spatial derivative of the mollified velocity is uniformly bounded by the input spatial L² norm.

theorem CKN.Leray.regularisedSchwartzMollify_iteratedLineDeriv_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) (n : ℕ) (m : Fin n → Foundation.Parabolic.L2Vec3) (x : Foundation.Parabolic.L2Vec3) : ‖(LineDeriv.iteratedLineDerivOp m (regularisedSchwartzMollify ρ ε hε ψ)) x‖ ≤ ‖(LineDeriv.iteratedLineDerivOp m (regularisedComplexMollifierSchwartz ρ ε hε)).toLp 2 MeasureTheory.volume‖ * ‖ψ.toLp 2 MeasureTheory.volume‖

Differentiating the mollified vector field in any finite ordered directions costs only the L² norm of the corresponding kernel derivative.