Uniform coordinate derivative constants for mollification

For each fixed order, one finite constant bounds every ordered coordinate derivative of the mollified velocity.

def CKN.Leray.regularisedSchwartzCoordinateDirection (i : Fin 3) : Foundation.Parabolic.L2Vec3

A CKN coordinate direction in the Fourier spatial carrier.

Equations

• CKN.Leray.regularisedSchwartzCoordinateDirection i = WithLp.toLp 2 (CKN.basisVec i)

def CKN.Leray.regularisedSchwartzCoordinateTuple {n : ℕ} (w : Fin n → Fin 3) : Fin n → Foundation.Parabolic.L2Vec3

An ordered tuple of Fourier spatial coordinate directions.

Equations

• CKN.Leray.regularisedSchwartzCoordinateTuple w k = CKN.Leray.regularisedSchwartzCoordinateDirection (w k)

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

The finite family of coordinate kernel directions used in the Schwartz mollifier estimate.

Equations

• One or more equations did not get rendered due to their size.

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

One constant, chosen before the velocity field, controls every ordered coordinate derivative of fixed-order Schwartz mollification.

theorem CKN.Leray.regularisedSchwartzMollify_coordinateDerivative_uniformBound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (n : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) (w : Fin n → Fin 3) (x : Foundation.Parabolic.L2Vec3), ‖(LineDeriv.iteratedLineDerivOp (regularisedSchwartzCoordinateTuple w) (regularisedSchwartzMollify ρ ε hε ψ)) x‖ ≤ C * ‖ψ.toLp 2 MeasureTheory.volume‖

For each derivative order, one finite nonnegative constant chosen before the velocity controls every ordered coordinate derivative.