Spatial differentiation of the Laplacian #
Ordered coordinate derivatives commute with each classical second coordinate derivative on all-order smooth scalar fields.
theorem
CKN.Leray.regularisedOrderedSpatialDerivative_comm_secondDerivative
(v : Foundation.Parabolic.Vec3 → ℝ)
(hv : ContDiff ℝ (↑⊤) v)
(α : List (Fin 3))
(i : Fin 3)
(x : Foundation.Parabolic.Vec3)
:
regularisedOrderedSpatialDerivative α
(fun (y : Foundation.Parabolic.Vec3) =>
(fderiv ℝ (fun (z : Foundation.Parabolic.Vec3) => (fderiv ℝ v z) (basisVec i)) y) (basisVec i))
x = (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => (fderiv ℝ (regularisedOrderedSpatialDerivative α v) y) (basisVec i))
x)
(basisVec i)
Every ordered derivative commutes with a classical second coordinate derivative of an all-order smooth scalar field.
theorem
CKN.Leray.regularisedOrderedSpatialDerivative_finset_sum
{ι : Type u_1}
(s : Finset ι)
(F : ι → Foundation.Parabolic.Vec3 → ℝ)
(hF : ∀ i ∈ s, ContDiff ℝ (↑⊤) (F i))
(α : List (Fin 3))
(x : Foundation.Parabolic.Vec3)
:
regularisedOrderedSpatialDerivative α (fun (y : Foundation.Parabolic.Vec3) => ∑ i ∈ s, F i y) x = ∑ i ∈ s, regularisedOrderedSpatialDerivative α (F i) x
Ordered coordinate derivatives distribute over a finite sum of all-order smooth scalar fields.
theorem
CKN.Leray.regularisedOrderedSpatialDerivative_comm_laplacian
(v : Foundation.Parabolic.Vec3 → ℝ)
(hv : ContDiff ℝ (↑⊤) v)
(α : List (Fin 3))
(x : Foundation.Parabolic.Vec3)
:
Every ordered coordinate derivative commutes with the classical Laplacian of an all-order smooth scalar field.
theorem
CKN.Leray.regularisedOrderedSpatialDerivative_laplacian_memLp
(v : Foundation.Parabolic.Vec3 → ℝ)
(hv : ContDiff ℝ (↑⊤) v)
(α : List (Fin 3))
(hDeriv :
∀ (β : List (Fin 3)),
β.length ≤ α.length + 2 → MeasureTheory.MemLp (regularisedOrderedSpatialDerivative β v) 2 MeasureTheory.volume)
:
The ordered derivative of the classical Laplacian is L² when the scalar has square-integrable ordered derivatives two orders higher.