Schwartz density in complete Bessel spaces

The Bessel/L² isometry transports density of Schwartz fields in L² to every complete Sobolev order.

theorem CKN.Leray.regularisedBesselSchwartzLift_denseRange (s : ℝ) : DenseRange fun (φ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) => BesselPotentialSpace.ofLp s (φ.toLp 2 MeasureTheory.volume)

Sobolev lifts of Schwartz L² fields are dense in every complete Bessel potential space.

theorem CKN.Leray.regularisedBesselSchwartzLift_hasSchwartzRepresentative (s : ℝ) (φ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) : ∃ (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3), ↑(BesselPotentialSpace.ofLp s (φ.toLp 2 MeasureTheory.volume)) = (SchwartzMap.toTemperedDistributionCLM Foundation.Parabolic.L2Vec3 ComplexVec3 MeasureTheory.volume) ψ

Lifting a Schwartz L² field into Hˢ still represents a Schwartz field: the inverse Bessel operator preserves Schwartz decay.