Physical equation of the linear complete Sobolev mild map

The H²ᵏ linear mild map realizes a complex L² Volterra equation with the same prescribed physical coefficient path.

theorem CKN.Leray.regularisedBesselLinearLocalMap_physical (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) (T : ℝ) (hT : 0 ≤ T) (g : C(↑(RegularizedMildTimeInterval T), ↥ComplexVectorL2)) (B : ℝ) (hB : 0 ≤ B) (hg : ∀ (q : ↑(RegularizedMildTimeInterval T)), ‖g q‖ ≤ B) (v : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)) (t : ↑(RegularizedMildTimeInterval T)) : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) ((regularisedBesselLinearLocalMap ρ ε hε k b T hT g B hB hg v) t) = heatSemigroup ↑t ⋯ ((regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) b) - ∫ (τ : ℝ) in 0..T, if h : 0 < τ ∧ τ < ↑t then stokesL2Operator ⋯ (((regularisedTensorPhysicalMap ρ ε hε) (g (regularizedMildTimeClamp T hT (↑t - τ)))) ((regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (v (regularizedMildTimeClamp T hT (↑t - τ))))) else 0

The complete Sobolev linear mild map represents the complex L² heat evolution and translated Stokes integral of its physical path.