L² representatives of Sobolev derivatives

An ordered spatial derivative through the Bessel order has a unique spatial L² representative. The representative is defined here so its linear and continuous dependence on the Sobolev field can be established.

noncomputable def CKN.Leray.regularisedBesselEvenOrderedDerivativeL2 (k : ℕ) (α : List Foundation.Parabolic.L2Vec3) (hα : α.length ≤ 2 * k) (v : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) : ↥ComplexVectorL2

The L² representative of an ordered distributional derivative of a Bessel field.

Equations

• CKN.Leray.regularisedBesselEvenOrderedDerivativeL2 k α hα v = Classical.choose ⋯

theorem CKN.Leray.regularisedBesselEvenOrderedDerivativeL2_toDistr (k : ℕ) (α : List Foundation.Parabolic.L2Vec3) (hα : α.length ≤ 2 * k) (v : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) : MeasureTheory.Lp.toTemperedDistribution (regularisedBesselEvenOrderedDerivativeL2 k α hα v) = (regularisedOrderedDistributionDerivativeCLM α) ↑v

The chosen L² field represents exactly the ordered derivative of the underlying Sobolev distribution.

theorem CKN.Leray.regularisedL2_toDistr_injective : Function.Injective fun (g : ↥ComplexVectorL2) => MeasureTheory.Lp.toTemperedDistribution g

noncomputable def CKN.Leray.regularisedBesselEvenOrderedDerivativeL2Linear (k : ℕ) (α : List Foundation.Parabolic.L2Vec3) (hα : α.length ≤ 2 * k) : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2 →ₗ[ℂ] ↥ComplexVectorL2

Ordered differentiation through the Bessel order is a complex-linear map from the Sobolev carrier to the physical spatial L² carrier.

Equations

• CKN.Leray.regularisedBesselEvenOrderedDerivativeL2Linear k α hα = { toFun := CKN.Leray.regularisedBesselEvenOrderedDerivativeL2 k α hα, map_add' := ⋯, map_smul' := ⋯ }

theorem CKN.Leray.regularisedBesselEvenOrderedDerivativeL2_continuous (k : ℕ) (α : List Foundation.Parabolic.L2Vec3) (hα : α.length ≤ 2 * k) : Continuous (regularisedBesselEvenOrderedDerivativeL2 k α hα)

The physical L² representative of an ordered Sobolev derivative is continuous in the complete Bessel norm.

noncomputable def CKN.Leray.regularisedBesselEvenOrderedDerivativeL2CLM (k : ℕ) (α : List Foundation.Parabolic.L2Vec3) (hα : α.length ≤ 2 * k) : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2 →L[ℂ] ↥ComplexVectorL2

Ordered spatial differentiation of an H^{2k} Bessel field is a bounded linear map to spatial L² through every order at most 2k.

Equations

• CKN.Leray.regularisedBesselEvenOrderedDerivativeL2CLM k α hα = { toLinearMap := CKN.Leray.regularisedBesselEvenOrderedDerivativeL2Linear k α hα, cont := ⋯ }

theorem CKN.Leray.regularisedBesselEvenOrderedDerivativeL2_norm_le (k : ℕ) (α : List Foundation.Parabolic.L2Vec3) (hα : α.length ≤ 2 * k) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (v : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2), ‖regularisedBesselEvenOrderedDerivativeL2 k α hα v‖ ≤ C * ‖v‖

Each ordered physical L² derivative through the Bessel order has a finite norm constant chosen independently of the Sobolev field.