Full Fréchet derivative bound for Schwartz mollification

Coordinate bounds for the differentiated mollifier control the full multilinear derivative norm uniformly in the velocity field.

noncomputable def CKN.Leray.regularisedSchwartzMollifyDerivative (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (n : ℕ) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) (x : Foundation.Parabolic.L2Vec3) : Foundation.Parabolic.L2Vec3 [×n]→L[ℝ] ComplexVec3

The full finite-order spatial derivative of a Schwartz mollified complex vector field.

Equations

• CKN.Leray.regularisedSchwartzMollifyDerivative ρ ε hε n ψ x = iteratedFDeriv ℝ n (⇑(CKN.Leray.regularisedSchwartzMollify ρ ε hε ψ)) x

noncomputable def CKN.Leray.regularisedSchwartzMollifyFullConstant (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (n : ℕ) : ℝ

The full derivative bound constant for mollifying a Schwartz function.

Equations

• CKN.Leray.regularisedSchwartzMollifyFullConstant ρ ε hε n = ↑(Fintype.card (Fin n → Fin 3)) * Classical.choose ⋯

theorem CKN.Leray.regularisedSchwartzMollify_iteratedFDeriv_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (n : ℕ) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) (x : Foundation.Parabolic.L2Vec3) : ‖regularisedSchwartzMollifyDerivative ρ ε hε n ψ x‖ ≤ regularisedSchwartzMollifyFullConstant ρ ε hε n * ‖ψ.toLp 2 MeasureTheory.volume‖

The full real Fréchet derivative of the complex Schwartz mollified velocity has a pointwise L²-input bound for every fixed order.

theorem CKN.Leray.regularisedSchwartzMollify_iteratedFDeriv_uniformBound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (n : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) (x : Foundation.Parabolic.L2Vec3), ‖regularisedSchwartzMollifyDerivative ρ ε hε n ψ x‖ ≤ C * ‖ψ.toLp 2 MeasureTheory.volume‖

A fixed mollifier and derivative order admit one nonnegative constant for every complex Schwartz velocity field and spatial point.