Realification of the shifted complete Sobolev mild integrand

If complete Sobolev and real physical velocity paths agree, their shifted Stokes integrands represent the same real physical vector.

theorem CKN.Leray.regularisedBesselShiftedStokesIntegrand_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 : ∀ (q : ↑(RegularizedMildTimeInterval T)), (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (u q) = complexifyVectorL2 (v q)) (t τ : ℝ) : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (regularisedBesselShiftedStokesIntegrand k (regularisedBesselClampedTensorPath ρ ε hε k T hT u) t τ) = complexifyVectorL2 (mildShiftedStokesIntegrand (regularizedMildClampedTensorTrajectory ρ ε hε T hT v) t τ)

The physical complete Sobolev shifted integrand is exactly the complexification of the real shifted mild integrand for the same path.