Bilinearity of the Schwartz tensor

Schwartz convolution and pointwise tensor pairing are linear in their respective inputs, so the regularized tensor is bilinear.

noncomputable def CKN.Leray.regularisedSchwartzMollifyLinear (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3 →ₗ[ℂ] SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3

Schwartz mollification by a fixed profile is complex linear.

Equations

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

theorem CKN.Leray.regularisedSchwartzMollifyLinear_apply (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (g : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) : (regularisedSchwartzMollifyLinear ρ ε hε) g = regularisedSchwartzMollify ρ ε hε g

The linear mollifier map agrees with Schwartz convolution.

noncomputable def CKN.Leray.regularisedSchwartzTensorBilinearLinear (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3 →ₗ[ℂ] SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3 →ₗ[ℂ] SchwartzMap Foundation.Parabolic.L2Vec3 ComplexTensor3

The regularized tensor with two Schwartz inputs is complex bilinear.

Equations

• CKN.Leray.regularisedSchwartzTensorBilinearLinear ρ ε hε = LinearMap.mk₂ ℂ (CKN.Leray.regularisedSchwartzTensorBilinear ρ ε hε) ⋯ ⋯ ⋯ ⋯

theorem CKN.Leray.regularisedSchwartzTensorBilinearLinear_apply (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (g f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) : ((regularisedSchwartzTensorBilinearLinear ρ ε hε) g) f = regularisedSchwartzTensorBilinear ρ ε hε g f

The bundled bilinear tensor has the original pointwise output.