The heat range in the Leray data space #
The heat multiplier preserves the divergence-free Fourier condition, which
places the real heat evolution of initial data in J.
theorem
CKN.Leray.realHeatOperator_isInJ
{t : ℝ}
(ht : 0 ≤ t)
(f : ↥RealVectorL2)
(hf : IsInJ (realVectorL2Representative f))
:
IsInJ (realVectorL2Representative (realHeatOperator t ht f))
The real heat semigroup preserves the Leray data space J.