Integration by parts for the regularized H¹ energy

Whole-space integration by parts for smooth fields with square-integrable derivatives, used to compare ‖∇U‖², ∫ U Δ U and ‖∇²U‖² in the differentiated energy identity (prop:lps-local-strong).

theorem ESS.LPS.lps_pairing_laplacian {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hf0 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hf1 : ∀ (j : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv f j) 2 MeasureTheory.volume) (hg1 : ∀ (j : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv g j) 2 MeasureTheory.volume) (hg2 : ∀ (j : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv (CKN.spatialDeriv g j) j) 2 MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), f x * CKN.spatialLaplacian g x = -∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv f j x * CKN.spatialDeriv g j x

Whole-space pairing of a smooth field with the Laplacian of another moves both derivatives: ∫ f Δg = -∑ⱼ ∫ ∂ⱼf ∂ⱼg (prop:lps-local-strong).

theorem ESS.LPS.lps_laplacian_sq_eq_hessian_sq {g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hL2 : ∀ (α : List (Fin 3)), α.length ≤ 3 → MeasureTheory.MemLp (CKN.wordDeriv α g) 2 MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialLaplacian g x ^ 2 = ∑ j : Fin 3, ∑ k : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv (CKN.spatialDeriv g j) k x ^ 2

For a smooth field with square-integrable derivatives through order three, ‖Δg‖₂² = ‖∇²g‖₂² (prop:lps-local-strong).

theorem ESS.LPS.lps_gradient_energy_difference {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hf0 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hf1 : ∀ (j : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv f j) 2 MeasureTheory.volume) (hf2 : ∀ (j : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv (CKN.spatialDeriv f j) j) 2 MeasureTheory.volume) (hg0 : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hg1 : ∀ (j : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv g j) 2 MeasureTheory.volume) (hg2 : ∀ (j : Fin 3), MeasureTheory.MemLp (CKN.spatialDeriv (CKN.spatialDeriv g j) j) 2 MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), (g x - f x) * -(CKN.spatialLaplacian f x + CKN.spatialLaplacian g x) = (∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv g j x ^ 2) - ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv f j x ^ 2

For smooth fields with square-integrable derivatives through order two, the change of the squared gradient norm is the pairing of the increment against minus the Laplacian of the sum (prop:lps-local-strong).

theorem ESS.LPS.lps_spatialLaplacian_eq_words (f : CKN.Foundation.Parabolic.Vec3 → ℝ) : CKN.spatialLaplacian f = fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, CKN.wordDeriv [j, j] f x

The Laplacian is the sum of the diagonal second ordered derivatives.

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

The Laplacian of a smooth function is smooth.

theorem ESS.LPS.lps_spatialDeriv_spatialLaplacian {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin 3) : CKN.spatialDeriv (CKN.spatialLaplacian f) i = fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, CKN.wordDeriv [j, j, i] f x

A derivative of the Laplacian is the sum of the diagonal third ordered derivatives.

theorem ESS.LPS.lps_spatialDeriv_spatialLaplacian_memLp {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hL2 : ∀ (α : List (Fin 3)), α.length ≤ 3 → MeasureTheory.MemLp (CKN.wordDeriv α f) 2 MeasureTheory.volume) (i : Fin 3) : MeasureTheory.MemLp (CKN.spatialDeriv (CKN.spatialLaplacian f) i) 2 MeasureTheory.volume

A derivative of the Laplacian of a smooth function with square-integrable derivatives through order three is square integrable.

theorem ESS.LPS.lps_spatialLaplacian_solenoidal {u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hu : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) (hdiv : ∀ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) i x = 0) (x : CKN.Foundation.Parabolic.Vec3) : ∑ i : Fin 3, CKN.spatialDeriv (CKN.spatialLaplacian fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) i x = 0

The componentwise Laplacian of a smooth solenoidal field is solenoidal (prop:lps-local-strong).