Semigroup law for the Fourier heat flow

The Gaussian frequency multiplier obeys the additive-time composition law. This identity is used when a mild trajectory is restarted at a later time.

theorem CKN.Leray.heatSymbol_add (s t : ℝ) (ξ : Foundation.Parabolic.L2Vec3) : heatSymbol (s + t) ξ = heatSymbol s ξ * heatSymbol t ξ

Gaussian heat symbols multiply when nonnegative time intervals are joined.

theorem CKN.Leray.regularisedHeatSemigroup_add (s t : ℝ) (hs : 0 ≤ s) (ht : 0 ≤ t) (f : ↥ComplexVectorL2) : heatSemigroup (s + t) ⋯ f = heatSemigroup s hs (heatSemigroup t ht f)

The complex Fourier heat flow composes across adjacent time intervals.