The Leibniz rule for the spatial Laplacian, in weak form

The paper's identity eq:leibniz-lap, Δ(η T) = η Δ T + 2 ∂_j η ∂_j T + T Δ η, is stated there for a scalar distribution T and a smooth η. This file proves the underlying pointwise second-order product rule for smooth functions on Vec3 := Fin 3 → ℝ, and then integrates it against a locally integrable weight to obtain the weak (test-function) form used in the paper.

Spatial partial derivatives are ordinary partial derivatives, expressed as the Fréchet derivative applied to a coordinate basis vector, matching the convention of CKN.spatialPartial.

Spatial partial derivatives and their product rules

noncomputable def CKN.spatialDeriv (f : Foundation.Parabolic.Vec3 → ℝ) (i : Fin 3) : Foundation.Parabolic.Vec3 → ℝ

The ith spatial partial derivative ∂_i f, as the Fréchet derivative applied to the ith coordinate basis vector.

Equations

• CKN.spatialDeriv f i x = (fderiv ℝ f x) (CKN.basisVec i)

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

The spatial Laplacian Δ f = ∑_i ∂_i ∂_i f.

Equations

• CKN.spatialLaplacian f x = ∑ i : Fin 3, CKN.spatialDeriv (CKN.spatialDeriv f i) i x

noncomputable def CKN.spatialGradDot (f g : Foundation.Parabolic.Vec3 → ℝ) : Foundation.Parabolic.Vec3 → ℝ

The Euclidean gradient pairing ∇f · ∇g = ∑_i ∂_i f ∂_i g.

Equations

• CKN.spatialGradDot f g x = ∑ i : Fin 3, CKN.spatialDeriv f i x * CKN.spatialDeriv g i x

noncomputable def CKN.mixedSecond (f : Foundation.Parabolic.Vec3 → ℝ) (i j : Fin 3) : Foundation.Parabolic.Vec3 → ℝ

The mixed second derivative ∂_i ∂_j f.

Equations

• CKN.mixedSecond f i j x = CKN.spatialDeriv (CKN.spatialDeriv f j) i x

theorem CKN.contDiff_spatialDeriv_smooth {f : Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin 3) : ContDiff ℝ (↑⊤) (spatialDeriv f i)

theorem CKN.contDiff_spatialLaplacian_smooth {f : Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (spatialLaplacian f)

theorem CKN.contDiff_spatialGradDot_smooth {f g : Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) : ContDiff ℝ (↑⊤) (spatialGradDot f g)

theorem CKN.contDiff_mixedSecond_smooth {f : Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i j : Fin 3) : ContDiff ℝ (↑⊤) (mixedSecond f i j)

theorem CKN.spatialDeriv_add {f g : Foundation.Parabolic.Vec3 → ℝ} {x : Foundation.Parabolic.Vec3} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (i : Fin 3) : spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => f y + g y) i x = spatialDeriv f i x + spatialDeriv g i x

theorem CKN.spatialDeriv_mul {f g : Foundation.Parabolic.Vec3 → ℝ} {x : Foundation.Parabolic.Vec3} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (i : Fin 3) : spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => f y * g y) i x = spatialDeriv f i x * g x + f x * spatialDeriv g i x

theorem CKN.spatialSecondDeriv_mul_smooth {η φ : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hφ : ContDiff ℝ (↑⊤) φ) (i j : Fin 3) (x : Foundation.Parabolic.Vec3) : mixedSecond (fun (y : Foundation.Parabolic.Vec3) => η y * φ y) i j x = mixedSecond η i j x * φ x + spatialDeriv η j x * spatialDeriv φ i x + spatialDeriv η i x * spatialDeriv φ j x + η x * mixedSecond φ i j x

The pointwise second-order product rule ∂_i ∂_j (η φ) of eq:leibniz-lap and eq:commute.

theorem CKN.spatialLaplacian_mul_smooth {η φ : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hφ : ContDiff ℝ (↑⊤) φ) : (spatialLaplacian fun (x : Foundation.Parabolic.Vec3) => η x * φ x) = fun (x : Foundation.Parabolic.Vec3) => η x * spatialLaplacian φ x + 2 * spatialGradDot η φ x + φ x * spatialLaplacian η x

The pointwise Leibniz rule eq:leibniz-lap for the spatial Laplacian: Δ(η φ) = η Δφ + 2 ∇η · ∇φ + φ Δη.