Translation of the shifted Stokes integral

An earlier Stokes interval in a restarted mild equation becomes the upper elapsed-time part after translating the integration variable.

theorem CKN.Leray.mildShiftedStokesIntegral_translate_upper (F : ℝ → ↥RealTensorL2) (a q : ℝ) (ha : 0 ≤ a) (hq : 0 ≤ q) : (∫ (τ : ℝ) in 0..a, if h : 0 < τ ∧ τ < a then realStokesOperator ⋯ (F (a - τ)) else 0) = ∫ (σ : ℝ) in q..a + q, mildShiftedStokesIntegrand F (a + q) σ

Translation by a nonnegative restart elapsed time identifies the propagated earlier Stokes kernels with the upper shifted interval.