The bounded linear Stokes action used in the mild integral

For each positive elapsed time, K(t) is a bounded linear map from tensor L² to velocity L², with the Abel-kernel bound from lem:reg-multiplier-bounds.

noncomputable def CKN.Leray.realStokesLinearMap {t : ℝ} (ht : 0 < t) : ↥RealTensorL2 →ₗ[ℝ] ↥RealVectorL2

The real-linear Stokes operator between tensor and vector L² spaces at positive time.

Equations

• CKN.Leray.realStokesLinearMap ht = { toFun := CKN.Leray.realStokesOperator ht, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def CKN.Leray.realStokesContinuousLinearMap {t : ℝ} (ht : 0 < t) : ↥RealTensorL2 →L[ℝ] ↥RealVectorL2

The continuous linear Stokes map at positive elapsed time.

Equations

• CKN.Leray.realStokesContinuousLinearMap ht = (CKN.Leray.realStokesLinearMap ht).mkContinuous (1 / √(2 * Real.exp 1 * t)) ⋯

theorem CKN.Leray.realStokesContinuousLinearMap_apply {t : ℝ} (ht : 0 < t) (F : ↥RealTensorL2) : (realStokesContinuousLinearMap ht) F = realStokesOperator ht F

Evaluation of the bounded linear Stokes map agrees with the Fourier defined operator.