Diffusive Sobolev energy pairing

The whole-space integration-by-parts identity gives the dissipative term for each ordered spatial derivative of the regularized equation.

noncomputable def CKN.Leray.regularisedScalarLaplacian (f : Foundation.Parabolic.Vec3 → ℝ) : Foundation.Parabolic.Vec3 → ℝ

The classical spatial Laplacian on a scalar field, written as the sum of its three coordinate second derivatives.

Equations

• CKN.Leray.regularisedScalarLaplacian f x = ∑ i : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ f y) (CKN.basisVec i)) x) (CKN.basisVec i)