Continuity of the regularized mild nonlinear and Stokes maps

These continuity statements are the time-regularity inputs to the Volterra construction in lem:reg-local-mild.

theorem CKN.Leray.regularizedMildTensor_continuousAt (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {α : Type u_1} {l : Filter α} (u : α → ↥RealVectorL2) (u₀ : ↥RealVectorL2) (hu : Filter.Tendsto u l (nhds u₀)) : Filter.Tendsto (fun (x : α) => regularizedMildTensor ρ ε hε (u x)) l (nhds (regularizedMildTensor ρ ε hε u₀))

The regularized quadratic tensor depends continuously on its velocity in spatial L², as required in lem:reg-local-mild.

theorem CKN.Leray.realStokesOperator_continuousAt_apply {t₀ : ℝ} (ht₀ : 0 < t₀) {α : Type u_1} {l : Filter α} (t : α → { x : ℝ // 0 < x }) (ht : Filter.Tendsto t l (nhds ⟨t₀, ht₀⟩)) (G : { x : ℝ // 0 < x } → ↥RealTensorL2) (hG : ContinuousAt G ⟨t₀, ht₀⟩) : Filter.Tendsto (fun (x : α) => realStokesOperator ⋯ (G (t x))) l (nhds (realStokesOperator ht₀ (G ⟨t₀, ht₀⟩)))

Applying the Stokes family to a continuous tensor path is continuous at every positive elapsed time; this is used for the integrand in lem:reg-local-mild.