Physical realization of the linear complete Sobolev tensor path

The tensor formed from a prescribed L² coefficient and a complete Sobolev path realizes the corresponding physical L² tensor.

theorem CKN.Leray.regularisedBesselLinearTensorPath_physical (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (T : ℝ) (hT : 0 ≤ T) (g : C(↑(RegularizedMildTimeInterval T), ↥ComplexVectorL2)) (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)) (s : ℝ) : (regularisedTensorBesselSobolevToL2 ↑(2 * k) ⋯) (regularisedBesselLinearTensorPath ρ ε hε k T hT g v s) = ((regularisedTensorPhysicalMap ρ ε hε) (g (regularizedMildTimeClamp T hT s))) ((regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (v (regularizedMildTimeClamp T hT s)))

The complete tensor path and the physical tensor agree at every time.