Linear Schwartz core of the Bessel potential space

The canonical Schwartz lift is linear, and its range is dense in the complete complex vector-valued Bessel space.

theorem CKN.Leray.regularisedBesselOfSchwartz_add (s : ℝ) (ψ χ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) : regularisedBesselOfSchwartz s (ψ + χ) = regularisedBesselOfSchwartz s ψ + regularisedBesselOfSchwartz s χ

The canonical vector Bessel lift is additive.

theorem CKN.Leray.regularisedBesselOfSchwartz_smul (s : ℝ) (c : ℂ) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) : regularisedBesselOfSchwartz s (c • ψ) = c • regularisedBesselOfSchwartz s ψ

The canonical vector Bessel lift commutes with complex scaling.

noncomputable def CKN.Leray.regularisedBesselSchwartzLinear (s : ℝ) : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3 →ₗ[ℂ] BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 s 2

The canonical vector Schwartz lift as a complex linear map.

Equations

• CKN.Leray.regularisedBesselSchwartzLinear s = { toFun := CKN.Leray.regularisedBesselOfSchwartz s, map_add' := ⋯, map_smul' := ⋯ }