Sobolev data as spatial L² fields

The bundled Bessel potential space is complete. At nonnegative order its inverse Fourier multiplier yields a spatial L² field with norm bounded by the Sobolev norm.

noncomputable def CKN.Leray.regularisedBesselInverseSymbol (s : ℝ) (p : Foundation.Parabolic.L2Vec3 × ComplexVec3) : ComplexVec3

The inverse Bessel-potential symbol acting on a complex Fourier vector.

Equations

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

theorem CKN.Leray.regularisedBesselInverseSymbol_measurable (s : ℝ) : Measurable (regularisedBesselInverseSymbol s)

theorem CKN.Leray.regularisedBesselInverseSymbol_norm_le (s : ℝ) (hs : 0 ≤ s) (ξ : Foundation.Parabolic.L2Vec3) (v : ComplexVec3) : ‖regularisedBesselInverseSymbol s (ξ, v)‖ ≤ ‖v‖

noncomputable def CKN.Leray.regularisedBesselFourierMultiplier (s : ℝ) (hs : 0 ≤ s) (F : ↥ComplexVectorL2) : ↥ComplexVectorL2

The bounded Fourier multiplier implementing the inverse Bessel weight on vector-valued fields.

Equations

• CKN.Leray.regularisedBesselFourierMultiplier s hs F = CKN.Leray.measurableFourierMultiplier (CKN.Leray.regularisedBesselInverseSymbol s) ⋯ 1 ⋯ F

theorem CKN.Leray.regularisedBesselFourierMultiplier_add (s : ℝ) (hs : 0 ≤ s) (F G : ↥ComplexVectorL2) : regularisedBesselFourierMultiplier s hs (F + G) = regularisedBesselFourierMultiplier s hs F + regularisedBesselFourierMultiplier s hs G

theorem CKN.Leray.regularisedBesselFourierMultiplier_smul (s : ℝ) (hs : 0 ≤ s) (c : ℂ) (F : ↥ComplexVectorL2) : regularisedBesselFourierMultiplier s hs (c • F) = c • regularisedBesselFourierMultiplier s hs F

noncomputable def CKN.Leray.regularisedBesselSobolevToL2 (s : ℝ) (hs : 0 ≤ s) (f : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 s 2) : ↥ComplexVectorL2

A nonnegative-order Bessel potential field determines a complex spatial L² field by applying the inverse Bessel weight in Fourier space.

Equations

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

theorem CKN.Leray.regularisedBesselSobolevToL2_fourier_ae (s : ℝ) (hs : 0 ≤ s) (f : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 s 2) : (fun (ξ : Foundation.Parabolic.L2Vec3) => ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (regularisedBesselSobolevToL2 s hs f)) ξ) =ᵐ[MeasureTheory.volume] fun (ξ : Foundation.Parabolic.L2Vec3) => ↑((1 + ‖ξ‖ ^ 2) ^ (-s / 2)) • ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) f.toLp) ξ

The Fourier transform of the physical L² realization is the inverse Bessel scalar weight times the weighted L² Fourier coordinate.

theorem CKN.Leray.regularisedBesselSobolevToL2_norm_le (s : ℝ) (hs : 0 ≤ s) (f : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 s 2) : ‖regularisedBesselSobolevToL2 s hs f‖ ≤ ‖f‖

The underlying spatial L² norm is at most the Bessel-potential Sobolev norm at every nonnegative order.

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

The nonnegative-order Bessel potential space embeds continuously into the complex spatial L² space through its inverse Fourier weight.

Equations

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

@[simp]

theorem CKN.Leray.regularisedBesselSobolevToL2CLM_apply (s : ℝ) (hs : 0 ≤ s) (f : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 s 2) : (regularisedBesselSobolevToL2CLM s hs) f = regularisedBesselSobolevToL2 s hs f

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

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

Equations

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

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

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

The L∞ representative of the inverse Bessel Fourier weight.

Equations

• CKN.Leray.regularisedBesselInverseWeightLp s hs = MeasureTheory.MemLp.toLp (CKN.Leray.regularisedBesselInverseWeight s) ⋯

theorem CKN.Leray.regularisedBesselSobolevToL2_toTemperedDistribution_eq (s : ℝ) (hs : 0 ≤ s) (f : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 s 2) : MeasureTheory.Lp.toTemperedDistribution (regularisedBesselSobolevToL2 s hs f) = ↑f

The inverse-weight L² field represents the underlying Bessel-potential tempered distribution.