Real physical form of the complete Sobolev mild map

The physical image of the complete local mild map is the complexification of the real local mild right-hand side for the same physical velocity path.

theorem CKN.Leray.regularisedBesselLocalMap_real_toLp (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (T : ℝ) (hT : 0 ≤ T) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) (b₀ : ↥RealVectorL2) (hb : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) b = complexifyVectorL2 b₀) (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 : ↑(RegularizedMildTimeInterval T)) : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) ((regularisedBesselLocalMap ρ ε hε k b T hT u) t) = complexifyVectorL2 (realHeatOperator ↑t ⋯ b₀ - ∫ (τ : ℝ) in 0..T, mildShiftedStokesIntegrand (regularizedMildClampedTensorTrajectory ρ ε hε T hT v) (↑t) τ)

The complete H²ᵏ local map represents the real heat evolution minus the real shifted Stokes integral of the same velocity path.