The mollifier kernel as a Schwartz field

The fixed smooth compactly supported mollifier defines a complex Schwartz scalar field on the Fourier spatial carrier.

theorem CKN.Leray.regularisedComplexMollifier_smooth (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : ContDiff ℝ ↑⊤ fun (x : Foundation.Parabolic.L2Vec3) => ↑(regMollifierKernel ρ ε hε x)

theorem CKN.Leray.regularisedComplexMollifier_compact (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : HasCompactSupport fun (x : Foundation.Parabolic.L2Vec3) => ↑(regMollifierKernel ρ ε hε x)

noncomputable def CKN.Leray.regularisedComplexMollifierSchwartz (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : SchwartzMap Foundation.Parabolic.L2Vec3 ℂ

The real mollifier kernel, embedded in the complex scalars, is a Schwartz field.

Equations

• CKN.Leray.regularisedComplexMollifierSchwartz ρ ε hε = ⋯.toSchwartzMap ⋯

theorem CKN.Leray.regularisedComplexMollifierSchwartz_apply (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (x : Foundation.Parabolic.L2Vec3) : (regularisedComplexMollifierSchwartz ρ ε hε) x = ↑(regMollifierKernel ρ ε hε x)

The Schwartz kernel agrees pointwise with the complexified regularized mollifier.