Physical realization of the complete tensor path

The complete Sobolev tensor path represents the real mild tensor path whenever the Sobolev and real velocity paths represent the same field.

theorem CKN.Leray.regularisedBesselClampedTensorPath_real_toLp (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)) (v : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)) (huv : ∀ (t : ↑(RegularizedMildTimeInterval T)), (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (u t) = complexifyVectorL2 (v t)) (s : ℝ) : (regularisedTensorBesselSobolevToL2 ↑(2 * k) ⋯) (regularisedBesselClampedTensorPath ρ ε hε k T hT u s) = complexifyTensorL2 (regularizedMildClampedTensorTrajectory ρ ε hε T hT v s)

Under pointwise physical agreement of two velocity paths, their clamped regularized tensors agree in physical L² at every real time.