Continuity of the force Duhamel integral

The Duhamel integral ∫₀ᵗ S(t-s) ℙ f(s) ds of eq:reg-mild-forced is a continuous curve in real L² for a force curve that is integrable on bounded intervals: at almost every fixed time the integrand is continuous in the evaluation time, and it is dominated by the norm of the force.

theorem CKN.Leray.norm_forcedRealInverse_le (w : ↥ComplexVectorL2) : ‖forcedRealInverse w‖ ≤ ‖w‖

theorem CKN.Leray.norm_forcedForceIntegrand_le (h : ℝ → ↥RealVectorL2) (t s : ℝ) : ‖forcedForceIntegrand h t s‖ ≤ ‖h s‖

theorem CKN.Leray.stronglyMeasurable_forcedForceIntegrand {h : ℝ → ↥RealVectorL2} (hh : MeasureTheory.StronglyMeasurable h) (t : ℝ) : MeasureTheory.StronglyMeasurable (forcedForceIntegrand h t)

theorem CKN.Leray.forcedHeatLeray_congr (w : ↥RealVectorL2) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a = b) : forcedHeatLeray a ha w = forcedHeatLeray b hb w

theorem CKN.Leray.continuousAt_forcedForceIntegrand (h : ℝ → ↥RealVectorL2) {s t₀ : ℝ} (hst : s ≠ t₀) : ContinuousAt (fun (t : ℝ) => forcedForceIntegrand h t s) t₀

At a fixed time different from the evaluation time, the force integrand is continuous in the evaluation time.

theorem CKN.Leray.continuous_forcedForceDuhamel {h : ℝ → ↥RealVectorL2} (hh : MeasureTheory.StronglyMeasurable h) (hH : ∀ (T : ℝ), MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖h s‖) (Set.Ioc 0 T) MeasureTheory.volume) : Continuous (forcedForceDuhamel h)

The force Duhamel integral of a force curve that is integrable on bounded intervals is continuous.