Bilinear regularized Schwartz tensors

Keeping the mollified and unmollified velocity fields distinct makes the quadratic tensor difference an exact two-term bilinear identity.

noncomputable def CKN.Leray.regularisedSchwartzTensorBilinear (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (g f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexTensor3

The regularized tensor with separate mollified and unmollified Schwartz velocity fields.

Equations

• CKN.Leray.regularisedSchwartzTensorBilinear ρ ε hε g f = ((SchwartzMap.pairing CKN.Leray.regularisedComplexTensorOuterCLM) (CKN.Leray.regularisedSchwartzMollify ρ ε hε g)) f

theorem CKN.Leray.regularisedSchwartzTensorBilinear_apply (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (g f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) (x : Foundation.Parabolic.L2Vec3) : (regularisedSchwartzTensorBilinear ρ ε hε g f) x = regularisedComplexTensorOuter ((regularisedSchwartzMollify ρ ε hε g) x) (f x)

The bilinear Schwartz tensor is the expected pointwise product.