Heat propagation of the Stokes operator

Applying heat flow after a Stokes operator adds the two elapsed times in the Fourier symbol. This is the kernel identity for splitting a Duhamel integral at a restart time.

theorem CKN.Leray.heatSymbol_smul_stokesFrequencySymbol (s t : ℝ) (ξ : Foundation.Parabolic.L2Vec3) (z : ComplexTensor3) : heatSymbol s ξ • (stokesFrequencySymbol t ξ) z = (stokesFrequencySymbol (s + t) ξ) z

The Gaussian factor of the Stokes symbol composes with heat flow.

theorem CKN.Leray.regularisedHeatSemigroup_stokesL2Operator (s t : ℝ) (hs : 0 ≤ s) (ht : 0 < t) (F : ↥ComplexTensorL2) : heatSemigroup s hs (stokesL2Operator ht F) = stokesL2Operator ⋯ F

Heat evolution of a Stokes output equals the Stokes output after the combined elapsed time.