The initial value of the mild trajectory

The heat multiplier is the identity at zero time, and the Stokes integral vanishes at zero time.

theorem CKN.Leray.realHeatOperator_zero (b : ↥RealVectorL2) : realHeatOperator 0 ⋯ b = b

The heat evolution at zero time is the identity on real spatial L².