Genuine Schwartz fields in complete Bessel spaces

The canonical Sobolev lift of a Schwartz distribution has dense range in every complete Bessel potential space.

noncomputable def CKN.Leray.regularisedBesselOfSchwartz (s : ℝ) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 s 2

The canonical complete Sobolev field represented by a Schwartz map.

Equations

• CKN.Leray.regularisedBesselOfSchwartz s ψ = ⋯.toBesselPotentialSpace

theorem CKN.Leray.regularisedBesselOfSchwartz_toDistr (s : ℝ) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) : ↑(regularisedBesselOfSchwartz s ψ) = (SchwartzMap.toTemperedDistributionCLM Foundation.Parabolic.L2Vec3 ComplexVec3 MeasureTheory.volume) ψ

The canonical Schwartz Sobolev lift represents the original Schwartz distribution.

theorem CKN.Leray.regularisedBesselSchwartzLift_range_subset (s : ℝ) : (Set.range fun (φ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) => BesselPotentialSpace.ofLp s (φ.toLp 2 MeasureTheory.volume)) ⊆ Set.range (regularisedBesselOfSchwartz s)

Every Bessel lift of a Schwartz L² field is represented by a Schwartz distribution in the same complete Sobolev space.