Realification of the heat and Stokes operators

The complex Fourier heat and Stokes operators applied to complexified real data are themselves complexifications of the corresponding real physical operators.

theorem CKN.Leray.heatSemigroup_complexify_real (t : ℝ) (ht : 0 ≤ t) (b : ↥RealVectorL2) : heatSemigroup t ht (complexifyVectorL2 b) = complexifyVectorL2 (realHeatOperator t ht b)

Heat evolution of real physical data remains in the real subspace of complex spatial L².

theorem CKN.Leray.stokesL2Operator_complexify_real {t : ℝ} (ht : 0 < t) (F : ↥RealTensorL2) : stokesL2Operator ht (complexifyTensorL2 F) = complexifyVectorL2 (realStokesOperator ht F)

The Stokes output of a real physical tensor remains in the real subspace of complex spatial L².