Canonical Bessel lifts of Schwartz tensor fields

The tensor produced by regularized Schwartz multiplication is lifted linearly into the complete Bessel potential space.

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

The complete Sobolev field represented by a complex Schwartz tensor.

Equations

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

theorem CKN.Leray.regularisedTensorBesselOfSchwartz_toDistr (s : ℝ) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexTensor3) : ↑(regularisedTensorBesselOfSchwartz s ψ) = (SchwartzMap.toTemperedDistributionCLM Foundation.Parabolic.L2Vec3 ComplexTensor3 MeasureTheory.volume) ψ

The canonical tensor lift retains its Schwartz distribution.

theorem CKN.Leray.regularisedTensorBesselOfSchwartz_add (s : ℝ) (ψ χ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexTensor3) : regularisedTensorBesselOfSchwartz s (ψ + χ) = regularisedTensorBesselOfSchwartz s ψ + regularisedTensorBesselOfSchwartz s χ

Canonical tensor Bessel lifting is additive.

theorem CKN.Leray.regularisedTensorBesselOfSchwartz_smul (s : ℝ) (c : ℂ) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexTensor3) : regularisedTensorBesselOfSchwartz s (c • ψ) = c • regularisedTensorBesselOfSchwartz s ψ

Canonical tensor Bessel lifting commutes with complex scaling.

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

The tensor Schwartz lift as a complex linear map.

Equations

• CKN.Leray.regularisedTensorBesselSchwartzLinear s = { toFun := CKN.Leray.regularisedTensorBesselOfSchwartz s, map_add' := ⋯, map_smul' := ⋯ }