Real physical realization of complete Sobolev heat evolution

Complete Bessel heat evolution from real physical initial data agrees with the real physical heat operator at every nonnegative time.

theorem CKN.Leray.regularisedBesselHeat_real_toLp (k : ℕ) (t : ℝ) (ht : 0 ≤ t) (b : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) (b₀ : ↥RealVectorL2) (hb : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) b = complexifyVectorL2 b₀) : (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (regularisedBesselHeat (↑(2 * k)) t ht b) = complexifyVectorL2 (realHeatOperator t ht b₀)

The physical field of complete H²ᵏ heat evolution of real data is the complexification of real heat evolution of that same datum.