Real heat and Stokes propagation laws

The real Fourier heat flow composes in time and propagates a real Stokes output by adding elapsed times.

theorem CKN.Leray.realHeatOperator_add (s t : ℝ) (hs : 0 ≤ s) (ht : 0 ≤ t) (b : ↥RealVectorL2) : realHeatOperator (s + t) ⋯ b = realHeatOperator s hs (realHeatOperator t ht b)

Real heat evolution composes across nonnegative adjacent times.

theorem CKN.Leray.realHeatOperator_stokes (s t : ℝ) (hs : 0 ≤ s) (ht : 0 < t) (F : ↥RealTensorL2) : realHeatOperator s hs (realStokesOperator ht F) = realStokesOperator ⋯ F

Real heat evolution of a Stokes output adds the two elapsed times.