Heat propagation of a real Stokes integral

Heat flow through the finite interval Stokes integral adds its elapsed time to each Stokes kernel.

theorem CKN.Leray.realHeatOperator_shiftedStokesIntegral (F : ℝ → ↥RealTensorL2) (hF : Continuous F) (C : ℝ) (hFC : ∀ (s : ℝ), ‖F s‖ ≤ C) (hC : 0 ≤ C) (a q : ℝ) (ha : 0 ≤ a) (hq : 0 ≤ q) : realHeatOperator q hq (∫ (τ : ℝ) in 0..a, mildShiftedStokesIntegrand F a τ) = ∫ (τ : ℝ) in 0..a, if h : 0 < τ ∧ τ < a then realStokesOperator ⋯ (F (a - τ)) else 0

Applying real heat flow to a translated Stokes integral adds the heat elapsed time to its Stokes kernel on the interval.