Regularized convolution on Schwartz velocity fields

The fixed complexified mollifier acts by Schwartz convolution on complex Schwartz vector fields.

noncomputable def CKN.Leray.regularisedSchwartzMollify (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3

Schwartz convolution with the complexified regularized mollifier.

Equations

• CKN.Leray.regularisedSchwartzMollify ρ ε hε ψ = ((SchwartzMap.convolution (ContinuousLinearMap.lsmul ℂ ℂ)) (CKN.Leray.regularisedComplexMollifierSchwartz ρ ε hε)) ψ

theorem CKN.Leray.regularisedSchwartzMollify_apply (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) (x : Foundation.Parabolic.L2Vec3) : (regularisedSchwartzMollify ρ ε hε ψ) x = MeasureTheory.convolution (fun (y : Foundation.Parabolic.L2Vec3) => ↑(regMollifierKernel ρ ε hε y)) (⇑ψ) (ContinuousLinearMap.lsmul ℂ ℂ) MeasureTheory.volume x

The Schwartz mollification equals pointwise convolution with the complexified real kernel.