Real velocities in the complex physical tensor map

The diagonal complex physical tensor is the complexification of the original real regularized mild nonlinearity.

theorem CKN.Leray.regularisedTensorPhysicalMap_real_diagonal (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) : ((regularisedTensorPhysicalMap ρ ε hε) (complexifyVectorL2 b)) (complexifyVectorL2 b) = complexifyTensorL2 (regularizedMildTensor ρ ε hε b)

The continuous complex bilinear tensor agrees with the real regularized mild tensor on the real L² subspace.