The bounded regularized tensor map on complete Sobolev spaces

The Schwartz estimate and the dense bilinear extension select one bounded tensor map on L² × H²ᵏ.

theorem CKN.Leray.regularisedBesselTensorExtension_exists (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∃ (F : ↥ComplexVectorL2 →L[ℂ] BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2 →L[ℂ] BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 (↑(2 * k)) 2), ‖F‖ ≤ C ∧ ∀ (g f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3), (F (g.toLp 2 MeasureTheory.volume)) (regularisedBesselOfSchwartz (↑(2 * k)) f) = regularisedTensorBesselOfSchwartz (↑(2 * k)) (regularisedSchwartzTensorBilinear ρ ε hε g f)

noncomputable def CKN.Leray.regularisedBesselTensorConstant (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) : ℝ

A finite nonnegative operator bound for the complete regularized tensor map at even Sobolev order.

Equations

• CKN.Leray.regularisedBesselTensorConstant ρ ε hε k = Classical.choose ⋯

noncomputable def CKN.Leray.regularisedBesselTensorMap (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) : ↥ComplexVectorL2 →L[ℂ] BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2 →L[ℂ] BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 (↑(2 * k)) 2

The complete H²ᵏ regularized tensor map, linear in both the spatial L² input and the complete H²ᵏ input.

Equations

• CKN.Leray.regularisedBesselTensorMap ρ ε hε k = Classical.choose ⋯

theorem CKN.Leray.regularisedBesselTensorMap_norm_le (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) : 0 ≤ regularisedBesselTensorConstant ρ ε hε k ∧ ‖regularisedBesselTensorMap ρ ε hε k‖ ≤ regularisedBesselTensorConstant ρ ε hε k

The chosen tensor operator has its advertised nonnegative bound.

theorem CKN.Leray.regularisedBesselTensorMap_schwartz (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (g f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) : ((regularisedBesselTensorMap ρ ε hε k) (g.toLp 2 MeasureTheory.volume)) (regularisedBesselOfSchwartz (↑(2 * k)) f) = regularisedTensorBesselOfSchwartz (↑(2 * k)) (regularisedSchwartzTensorBilinear ρ ε hε g f)

On Schwartz data, the complete tensor map equals the canonical Bessel lift of the original Schwartz product.