Restart identity for a real Duhamel expression

The heat semigroup propagates the initial value and the earlier Stokes integral, leaving only the later Stokes contribution after a restart.

theorem CKN.Leray.regularisedRealDuhamel_restart (F : ℝ → ↥RealTensorL2) (hF : Continuous F) (C : ℝ) (hFC : ∀ (s : ℝ), ‖F s‖ ≤ C) (hC : 0 ≤ C) (b : ↥RealVectorL2) (a q : ℝ) (ha : 0 ≤ a) (hq : 0 ≤ q) : realHeatOperator q hq (realHeatOperator a ha b - ∫ (τ : ℝ) in 0..a, mildShiftedStokesIntegrand F a τ) - ∫ (τ : ℝ) in 0..q, mildShiftedStokesIntegrand F (a + q) τ = realHeatOperator (a + q) ⋯ b - ∫ (τ : ℝ) in 0..a + q, mildShiftedStokesIntegrand F (a + q) τ

The regularized Duhamel expression has the semigroup restart law for every continuous uniformly bounded tensor path.