Stokes operator on complete Bessel coordinates

The Fourier Stokes multiplier acts on the weighted L² coordinates of complete Bessel spaces with the same integrable Abel-kernel bound.

noncomputable def CKN.Leray.regularisedStokesL2CLM {t : ℝ} (ht : 0 < t) : ↥ComplexTensorL2 →L[ℂ] ↥ComplexVectorL2

The complex L² Stokes operator as a bounded complex linear map.

Equations

• CKN.Leray.regularisedStokesL2CLM ht = { toFun := CKN.Leray.stokesL2Operator ht, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (1 / √(2 * Real.exp 1 * t)) ⋯

noncomputable def CKN.Leray.regularisedBesselStokesOperator {t : ℝ} (ht : 0 < t) (k : ℕ) : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 (↑(2 * k)) 2 →L[ℂ] BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2

The complete H²ᵏ Stokes operator on weighted Bessel coordinates.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.regularisedBesselStokesOperator_norm_le {t : ℝ} (ht : 0 < t) (k : ℕ) (F : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 (↑(2 * k)) 2) : ‖(regularisedBesselStokesOperator ht k) F‖ ≤ 1 / √(2 * Real.exp 1 * t) * ‖F‖

The complete H²ᵏ Stokes operator has the same Abel-kernel bound as the underlying L² multiplier.

theorem CKN.Leray.regularisedBesselStokesOperator_continuousAt_apply {t₀ : ℝ} (ht₀ : 0 < t₀) (k : ℕ) (F : { x : ℝ // 0 < x } → BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 (↑(2 * k)) 2) (hF : ContinuousAt F ⟨t₀, ht₀⟩) : ContinuousAt (fun (t : { x : ℝ // 0 < x }) => (regularisedBesselStokesOperator ⋯ k) (F t)) ⟨t₀, ht₀⟩

The complete Sobolev Stokes output is continuous when both the positive elapsed time and its tensor input vary continuously.