Physical realization of the shifted complete Sobolev integral

For corresponding complete Sobolev and real physical velocity paths, their shifted Stokes integrals agree after physical realization and complexification.

theorem CKN.Leray.regularisedBesselShiftedStokesIntegral_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)) (R : ℝ) (hR : 0 ≤ R) (hu : ∀ (q : ↑(RegularizedMildTimeInterval T)), ‖u q‖ ≤ R) (hv : ∀ (q : ↑(RegularizedMildTimeInterval T)), ‖v q‖ ≤ R) (t : ℝ) : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (∫ (τ : ℝ) in 0..T, regularisedBesselShiftedStokesIntegrand k (regularisedBesselClampedTensorPath ρ ε hε k T hT u) t τ) = complexifyVectorL2 (∫ (τ : ℝ) in 0..T, mildShiftedStokesIntegrand (regularizedMildClampedTensorTrajectory ρ ε hε T hT v) t τ)

The physical L² realization of the complete shifted Stokes integral is the complexification of the real shifted mild integral.