Compatibility of the Sobolev and physical tensor maps

The bounded tensor map on L² × H²ᵏ represents the bounded physical bilinear tensor on the underlying spatial L² fields.

theorem CKN.Leray.regularisedBesselTensorMap_physical (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (g : ↥ComplexVectorL2) (f : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) : (regularisedTensorBesselSobolevToL2 ↑(2 * k) ⋯) (((regularisedBesselTensorMap ρ ε hε k) g) f) = ((regularisedTensorPhysicalMap ρ ε hε) g) ((regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) f)

The complete tensor map and the physical L² tensor map agree on every L² × H²ᵏ pair after taking the physical realization.