Extension of the regularized tensor to complete Sobolev data

The Schwartz tensor's bilinear H²ᵏ bound extends uniquely to L² × H²ᵏ with the same operator norm.

noncomputable def CKN.Leray.regularisedSchwartzTensorBilinearBesselLinear (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (s : ℝ) : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3 →ₗ[ℂ] SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3 →ₗ[ℂ] BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 s 2

The canonical complete tensor lift of the Schwartz bilinear regularized nonlinearity is itself bilinear.

Equations

• CKN.Leray.regularisedSchwartzTensorBilinearBesselLinear ρ ε hε s = (CKN.Leray.regularisedSchwartzTensorBilinearLinear ρ ε hε).compr₂ₛₗ (CKN.Leray.regularisedTensorBesselSchwartzLinear s)

theorem CKN.Leray.regularisedSchwartzTensorBilinearBesselLinear_apply (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (s : ℝ) (g f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3) : ((regularisedSchwartzTensorBilinearBesselLinear ρ ε hε s) g) f = regularisedTensorBesselOfSchwartz s (regularisedSchwartzTensorBilinear ρ ε hε g f)

The bundled Bessel tensor map is the canonical lift of the regularized Schwartz tensor.

theorem CKN.Leray.regularisedSchwartzTensorBilinear_bessel_even_extension_of_bound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (k : ℕ) (hB : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (g f : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3), ‖⋯.toBesselPotentialSpace‖ ≤ C * ‖g.toLp 2 MeasureTheory.volume‖ * ‖regularisedBesselOfSchwartz (↑(2 * k)) f‖) : ∃ (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)

The H²ᵏ tensor estimate on Schwartz fields yields a bounded bilinear map from spatial L² × complete H²ᵏ into complete tensor H²ᵏ.