Strong time continuity of the regularized Stokes operator

The Fourier multiplier for the Stokes operator is strongly continuous at positive elapsed times, as used in lem:reg-local-mild.

noncomputable def CKN.Leray.stokesFormulaField (t : ℝ) (F : ↥ComplexTensorL2) : Foundation.Parabolic.L2Vec3 → ComplexVec3

The Fourier-side vector field obtained by applying the Stokes formula at each frequency.

Equations

• CKN.Leray.stokesFormulaField t F ξ = CKN.Leray.stokesApplyFormula t ξ (↑↑F ξ)

theorem CKN.Leray.stokesFourierMultiplier_continuousAt {t₀ : ℝ} (ht₀ : 0 < t₀) (F : ↥ComplexTensorL2) : ContinuousAt (fun (t : { t : ℝ // 0 < t }) => stokesFourierMultiplier ⋯ F) ⟨t₀, ht₀⟩

The frequency-side Stokes multiplier is strongly continuous on each fixed tensor input at positive elapsed times.

theorem CKN.Leray.realStokesOperator_continuousAt {t₀ : ℝ} (ht₀ : 0 < t₀) (F : ↥RealTensorL2) : ContinuousAt (fun (t : { t : ℝ // 0 < t }) => realStokesOperator ⋯ F) ⟨t₀, ht₀⟩

The physical real Stokes operator is strongly continuous at positive elapsed times.