Truncating the real shifted Stokes integral

The translated real Stokes integrand vanishes after its observation time, so later integration limits give the same value.

theorem CKN.Leray.mildShiftedStokesIntegral_truncate (F : ℝ → ↥RealTensorL2) (T t : ℝ) (ht : 0 ≤ t) (htT : t ≤ T) (hInt : IntervalIntegrable (mildShiftedStokesIntegrand F t) MeasureTheory.volume 0 T) : ∫ (τ : ℝ) in 0..T, mildShiftedStokesIntegrand F t τ = ∫ (τ : ℝ) in 0..t, mildShiftedStokesIntegrand F t τ

A shifted real Stokes integral only uses elapsed times before its observation time.