The regularized tensor of Schwartz velocity fields

The outer product is a continuous complex bilinear map. Pairing it with Schwartz mollification preserves Schwartz regularity of the tensor.

def CKN.Leray.regularisedComplexTensorOuter (v u : ComplexVec3) : ComplexTensor3

The componentwise outer product on complex Euclidean three-vectors.

Equations

• CKN.Leray.regularisedComplexTensorOuter v u = WithLp.toLp 2 fun (i : Fin 3) => WithLp.toLp 2 fun (j : Fin 3) => v.ofLp i * u.ofLp j

theorem CKN.Leray.regularisedComplexTensorOuter_norm (v u : ComplexVec3) : ‖regularisedComplexTensorOuter v u‖ = ‖v‖ * ‖u‖

The Frobenius norm of a complex rank-one tensor is the product of the two vector norms.

def CKN.Leray.regularisedComplexTensorOuterLinear : ComplexVec3 →ₗ[ℂ] ComplexVec3 →ₗ[ℂ] ComplexTensor3

The complex-bilinear map forming the outer product of two complex vector values.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.Leray.regularisedComplexTensorOuterCLM : ComplexVec3 →L[ℂ] ComplexVec3 →L[ℂ] ComplexTensor3

The complex rank-one tensor is a continuous bilinear map on the Euclidean spatial carriers.

Equations

• CKN.Leray.regularisedComplexTensorOuterCLM = CKN.Leray.regularisedComplexTensorOuterLinear.mkContinuous₂ 1 CKN.Leray.regularisedComplexTensorOuterCLM._proof_1

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

The regularized quadratic tensor of a complex Schwartz velocity field is again Schwartz.

Equations

• CKN.Leray.regularisedSchwartzTensor ρ ε hε ψ = ((SchwartzMap.pairing CKN.Leray.regularisedComplexTensorOuterCLM) (CKN.Leray.regularisedSchwartzMollify ρ ε hε ψ)) ψ

theorem CKN.Leray.regularisedSchwartzTensor_apply (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) (x : Foundation.Parabolic.L2Vec3) : (regularisedSchwartzTensor ρ ε hε ψ) x = regularisedComplexTensorOuter ((regularisedSchwartzMollify ρ ε hε ψ) x) (ψ x)

The Schwartz tensor has the expected pointwise outer-product form.