Heat evolution of the projected tensor divergence

The Fourier formulas show that heat evolution composes with the regularized Leray--Stokes operator by adding elapsed times.

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

The complex Stokes operator is strongly continuous at every positive elapsed time for a fixed tensor input.

theorem CKN.Leray.stokesL2Operator_continuousAt_apply {t₀ : ℝ} (ht₀ : 0 < t₀) {α : Type u_1} {l : Filter α} (t : α → { x : ℝ // 0 < x }) (ht : Filter.Tendsto t l (nhds ⟨t₀, ht₀⟩)) (F : { x : ℝ // 0 < x } → ↥ComplexTensorL2) (hF : ContinuousAt F ⟨t₀, ht₀⟩) : Filter.Tendsto (fun (x : α) => stokesL2Operator ⋯ (F (t x))) l (nhds (stokesL2Operator ht₀ (F ⟨t₀, ht₀⟩)))

Applying the complex Stokes family to a continuous tensor path is continuous at every positive elapsed time.