Realification of Schwartz mollification

The complex Schwartz convolution of a real Schwartz field is the complexification of the real regularized convolution.

theorem CKN.Leray.regularisedSchwartzMollify_complexifyReal_apply (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (φ : SchwartzMap Foundation.Parabolic.L2Vec3 Foundation.Parabolic.L2Vec3) (x : Foundation.Parabolic.L2Vec3) : (regularisedSchwartzMollify ρ ε hε (complexifyRealSchwartz φ)) x = complexifyValue (regMollifyVector ρ ε hε (⇑φ) x)

Complexification commutes with convolution by the real mollifier on Schwartz velocity fields.

theorem CKN.Leray.regularisedSchwartzTensor_complexifyReal_apply (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (φ : SchwartzMap Foundation.Parabolic.L2Vec3 Foundation.Parabolic.L2Vec3) (x : Foundation.Parabolic.L2Vec3) : (regularisedSchwartzTensor ρ ε hε (complexifyRealSchwartz φ)) x = complexifyTensorValue (regularizedTensorOuter (regMollifyVector ρ ε hε (⇑φ) x) (φ x))

The complex Schwartz tensor of a real Schwartz velocity agrees pointwise with the complexification of the real mild tensor field.

theorem CKN.Leray.regularisedSchwartzTensor_complexifyReal_toLp (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (φ : SchwartzMap Foundation.Parabolic.L2Vec3 Foundation.Parabolic.L2Vec3) : (regularisedSchwartzTensor ρ ε hε (complexifyRealSchwartz φ)).toLp 2 MeasureTheory.volume = complexifyTensorL2 (regularizedMildTensor ρ ε hε (φ.toLp 2 MeasureTheory.volume))

On real Schwartz data, the complex Schwartz tensor represents the same L² class as the complexified real mild nonlinearity.