The complete quadratic tensor represents the real mild tensor

A complete Sobolev velocity whose physical field is real has exactly the original real regularized tensor as its physical nonlinear output.

theorem CKN.Leray.regularisedBesselTensorQuadratic_real_toLp (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (u : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) (b : ↥RealVectorL2) (hu : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) u = complexifyVectorL2 b) : (regularisedTensorBesselSobolevToL2 ↑(2 * k) ⋯) (regularisedBesselTensorQuadratic ρ ε hε k u) = complexifyTensorL2 (regularizedMildTensor ρ ε hε b)

The quadratic complete tensor agrees in physical L² with the regularized mild tensor of the same real velocity.