Physical realization of the shifted complete Stokes integrand

The complete Sobolev shifted Stokes integrand represents the physical complex L² shifted Stokes integrand at every pair of times.

theorem CKN.Leray.regularisedBesselShiftedStokesIntegrand_physical (k : ℕ) (F : ℝ → BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 (↑(2 * k)) 2) (t τ : ℝ) : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (regularisedBesselShiftedStokesIntegrand k F t τ) = if h : 0 < τ ∧ τ < t then stokesL2Operator ⋯ ((regularisedTensorBesselSobolevToL2 ↑(2 * k) ⋯) (F (t - τ))) else 0

Taking the physical realization commutes pointwise with the shifted complete Sobolev Stokes integrand.