The mollified initial state in the Leray space

Convolution with the smooth compactly supported profile in eq:reg-mollifier preserves the divergence-free space used in lem:reg-local-mild.

def CKN.Leray.regularisedCoordinateEquiv : Foundation.Parabolic.L2Vec3 ≃L[ℝ] Foundation.Parabolic.Vec3

The continuous coordinate equivalence for the regularized initial-data construction.

Equations

• CKN.Leray.regularisedCoordinateEquiv = PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin 3) => ℝ

noncomputable def CKN.Leray.regularisedPhysicalKernel (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : Foundation.Parabolic.Vec3 → ℝ

The physical-space regularized convolution kernel.

Equations

• CKN.Leray.regularisedPhysicalKernel ρ ε hε x = CKN.Leray.regMollifierKernel ρ ε hε (WithLp.toLp 2 x)

noncomputable def CKN.Leray.regularisedScalarConvolution (κ f : Foundation.Parabolic.Vec3 → ℝ) : Foundation.Parabolic.Vec3 → ℝ

Scalar convolution by the dilated regularized mollifier kernel.

Equations

• CKN.Leray.regularisedScalarConvolution κ f = MeasureTheory.convolution κ f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

def CKN.Leray.regularisedVectorActionLinear : ℝ →ₗ[ℝ] Foundation.Parabolic.L2Vec3 →ₗ[ℝ] Foundation.Parabolic.L2Vec3

The bilinear scalar action on vector-valued functions used by regularized convolution.

Equations

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

noncomputable def CKN.Leray.regularisedVectorAction : ℝ →L[ℝ] Foundation.Parabolic.L2Vec3 →L[ℝ] Foundation.Parabolic.L2Vec3

The continuous scalar action on vector-valued L² functions.

Equations

• CKN.Leray.regularisedVectorAction = CKN.Leray.regularisedVectorActionLinear.mkContinuous₂ 1 CKN.Leray.regularisedVectorAction._proof_1

noncomputable def CKN.Leray.regularisedProfileConvolution (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

Convolution of a scalar profile with vector-valued initial data.

Equations

• CKN.Leray.regularisedProfileConvolution ρ ε hε a x i = CKN.Leray.regularisedScalarConvolution (CKN.Leray.regularisedPhysicalKernel ρ ε hε) (fun (y : CKN.Foundation.Parabolic.Vec3) => a y i) x

def CKN.Leray.regularisedCoordinateTuple (n : ℕ) (w : Fin n → Fin 3) : Fin n → Foundation.Parabolic.Vec3

The tuple of coordinate functions associated with the regularized vector data.

Equations

• CKN.Leray.regularisedCoordinateTuple n w j = CKN.basisVec (w j)

theorem CKN.Leray.regularisedScalarConvolution_iterated_derivative (n : ℕ) (w : Fin n → Fin 3) (κ : Foundation.Parabolic.Vec3 → ℝ) (hκ : ContDiff ℝ (↑⊤) κ) (hκc : HasCompactSupport κ) {f : Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (x : Foundation.Parabolic.Vec3) : ((iteratedFDeriv ℝ n (MeasureTheory.convolution κ f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) x) fun (j : Fin n) => basisVec (w j)) = MeasureTheory.convolution (fun (y : Foundation.Parabolic.Vec3) => (iteratedFDeriv ℝ n κ y) fun (j : Fin n) => basisVec (w j)) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

Ordered derivatives commute with convolution by a smooth compactly supported scalar kernel, as in lem:reg-mollifier-bounds.

theorem CKN.Leray.regUniformMollifiedInitial_component_convolution (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) (x : Foundation.Parabolic.Vec3) (i : Fin 3) : regUniformMollifiedInitial ρ ε hε a x i = MeasureTheory.convolution (fun (y : Foundation.Parabolic.Vec3) => regMollifierKernel ρ ε hε (WithLp.toLp 2 y)) (fun (y : Foundation.Parabolic.Vec3) => a y i) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x

Each component of the mollified state is the scalar convolution of the physical kernel with the corresponding input component, as in lem:reg-mollifier-bounds.

theorem CKN.Leray.regUniformMollifiedInitial_coordinateDerivative_memLp (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) (n : ℕ) (w : Fin n → Fin 3) (i : Fin 3) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => (iteratedFDeriv ℝ n (fun (z : Foundation.Parabolic.Vec3) => regUniformMollifiedInitial ρ ε hε a z i) x) fun (j : Fin n) => basisVec (w j)) 2 MeasureTheory.volume

Every ordered spatial derivative of the mollified initial state in eq:reg-mollifier remains square integrable; this is the initial Sobolev input for the regularized evolution in thm:regularised.

theorem CKN.Leray.regMollifiedInitial_isInJ (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) : IsInJ (regUniformMollifiedInitial ρ ε hε a)

Convolution by the smooth compactly supported profile in eq:reg-mollifier preserves the Leray space J.