Tensor Bessel-potential fields as spatial L² fields

At nonnegative order, the inverse tensor Bessel multiplier realizes a complete Bessel-potential field as a spatial L² tensor. The realization agrees with the canonical lift of every Schwartz tensor.

noncomputable def CKN.Leray.regularisedTensorBesselInverseSymbol (s : ℝ) (p : Foundation.Parabolic.L2Vec3 × ComplexTensor3) : ComplexTensor3

The inverse Bessel-potential symbol acting on a complex tensor frequency value.

Equations

• CKN.Leray.regularisedTensorBesselInverseSymbol s p = ↑((1 + ‖p.1‖ ^ 2) ^ (-s / 2)) • p.2

theorem CKN.Leray.regularisedTensorBesselInverseSymbol_measurable (s : ℝ) : Measurable (regularisedTensorBesselInverseSymbol s)

theorem CKN.Leray.regularisedTensorBesselInverseSymbol_norm_le (s : ℝ) (hs : 0 ≤ s) (ξ : Foundation.Parabolic.L2Vec3) (v : ComplexTensor3) : ‖regularisedTensorBesselInverseSymbol s (ξ, v)‖ ≤ ‖v‖

noncomputable def CKN.Leray.regularisedTensorBesselFourierMultiplier (s : ℝ) (hs : 0 ≤ s) (F : ↥ComplexTensorL2) : ↥ComplexTensorL2

The bounded Fourier multiplier implementing the inverse Bessel weight on tensor fields.

Equations

• CKN.Leray.regularisedTensorBesselFourierMultiplier s hs F = CKN.Leray.measurableFourierMultiplier (CKN.Leray.regularisedTensorBesselInverseSymbol s) ⋯ 1 ⋯ F

theorem CKN.Leray.regularisedTensorBesselFourierMultiplier_add (s : ℝ) (hs : 0 ≤ s) (F G : ↥ComplexTensorL2) : regularisedTensorBesselFourierMultiplier s hs (F + G) = regularisedTensorBesselFourierMultiplier s hs F + regularisedTensorBesselFourierMultiplier s hs G

theorem CKN.Leray.regularisedTensorBesselFourierMultiplier_smul (s : ℝ) (hs : 0 ≤ s) (c : ℂ) (F : ↥ComplexTensorL2) : regularisedTensorBesselFourierMultiplier s hs (c • F) = c • regularisedTensorBesselFourierMultiplier s hs F

noncomputable def CKN.Leray.regularisedTensorBesselSobolevToL2Fun (s : ℝ) (hs : 0 ≤ s) (F : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 s 2) : ↥ComplexTensorL2

The L² function obtained from a tensor Bessel-potential element by its Fourier multiplier.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.regularisedTensorBesselSobolevToL2_norm_le_fun (s : ℝ) (hs : 0 ≤ s) (F : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 s 2) : ‖regularisedTensorBesselSobolevToL2Fun s hs F‖ ≤ ‖F‖

noncomputable def CKN.Leray.regularisedTensorBesselSobolevToL2 (s : ℝ) (hs : 0 ≤ s) : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexTensor3 s 2 →L[ℂ] ↥ComplexTensorL2

A nonnegative-order tensor Bessel-potential field determines its spatial L² representative by the inverse Bessel weight in Fourier space.

Equations

• CKN.Leray.regularisedTensorBesselSobolevToL2 s hs = { toFun := CKN.Leray.regularisedTensorBesselSobolevToL2Fun s hs, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

noncomputable def CKN.Leray.regularisedTensorBesselInverseWeight (s : ℝ) (ξ : Foundation.Parabolic.L2Vec3) : ℂ

The scalar Fourier weight defining the inverse tensor Bessel-potential operator.

Equations

• CKN.Leray.regularisedTensorBesselInverseWeight s ξ = ↑((1 + ‖ξ‖ ^ 2) ^ (-s / 2))

theorem CKN.Leray.regularisedTensorBesselInverseWeight_memLp (s : ℝ) (hs : 0 ≤ s) : MeasureTheory.MemLp (regularisedTensorBesselInverseWeight s) ⊤ MeasureTheory.volume

noncomputable def CKN.Leray.regularisedTensorBesselInverseWeightLp (s : ℝ) (hs : 0 ≤ s) : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)

The L∞ representative of the inverse tensor Bessel Fourier weight.

Equations

• CKN.Leray.regularisedTensorBesselInverseWeightLp s hs = MeasureTheory.MemLp.toLp (CKN.Leray.regularisedTensorBesselInverseWeight s) ⋯

theorem CKN.Leray.regularisedTensorBesselSobolevToL2_schwartz (s : ℝ) (hs : 0 ≤ s) (ψ : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexTensor3) : (regularisedTensorBesselSobolevToL2 s hs) (regularisedTensorBesselOfSchwartz s ψ) = ψ.toLp 2 MeasureTheory.volume

The inverse Bessel-weighted tensor L² field agrees with the canonical Bessel lift of a Schwartz tensor.