Physical realization of the shifted complete Stokes integral

The complete Sobolev Stokes integral represents the corresponding complex spatial L² integral.

theorem CKN.Leray.regularisedBesselShiftedStokesIntegral_physical (k : ℕ) (F : ℝ → BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 (↑(2 * k)) 2) (hF : Continuous F) (C : ℝ) (hFC : ∀ (s : ℝ), ‖F s‖ ≤ C) (hC : 0 ≤ C) (T t : ℝ) (hT : 0 ≤ T) : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (∫ (τ : ℝ) in 0..T, regularisedBesselShiftedStokesIntegrand k F t τ) = ∫ (τ : ℝ) in 0..T, if h : 0 < τ ∧ τ < t then stokesL2Operator ⋯ ((regularisedTensorBesselSobolevToL2 ↑(2 * k) ⋯) (F (t - τ))) else 0

The physical realization commutes with a shifted complete Sobolev Stokes integral over a bounded interval.