Green's identity for the truncated spatial Laplacian

This file proves the integration-by-parts identity needed for the comparison energy inequality: moving one derivative from the truncated Laplacian partialLaplacian onto a second compactly supported test function. This is the missing ingredient for integrating the mollified equation against a Kato test function in the mollified comparison equation.

theorem CIV.contDiff_gradPair_of_contDiff {m : ℕ} {φ : CKN.Vec m × ℝ → ℝ} {τ : ℝ} (hφ : ContDiff ℝ ↑⊤ fun (x : CKN.Vec m) => φ (x, τ)) (i : Fin m) : ContDiff ℝ ↑⊤ fun (x : CKN.Vec m) => gradPair m φ (x, τ) (CKN.basisVec i)

The spatial gradient paired with a basis vector is smooth when the test function is smooth on each time slice.

theorem CIV.hasCompactSupport_gradPair_of_hasCompactSupport {m : ℕ} {φ : CKN.Vec m × ℝ → ℝ} {τ : ℝ} (hsupp : HasCompactSupport fun (x : CKN.Vec m) => φ (x, τ)) (i : Fin m) : HasCompactSupport fun (x : CKN.Vec m) => gradPair m φ (x, τ) (CKN.basisVec i)

The spatial gradient paired with a basis vector has compact support when the test function does.

theorem CIV.integral_gradPair_deriv_mul_eq_neg_integral_gradPair_mul {m : ℕ} {φ ψ : CKN.Vec m × ℝ → ℝ} {τ : ℝ} (hφ : ContDiff ℝ ↑⊤ fun (x : CKN.Vec m) => φ (x, τ)) (hψ : ContDiff ℝ ↑⊤ fun (x : CKN.Vec m) => ψ (x, τ)) (hφsupp : HasCompactSupport fun (x : CKN.Vec m) => φ (x, τ)) (i : Fin m) : ∫ (x : CKN.Vec m), (fderiv ℝ (fun (y : CKN.Vec m) => gradPair m φ (y, τ) (CKN.basisVec i)) x) (CKN.basisVec i) * ψ (x, τ) = -∫ (x : CKN.Vec m), gradPair m φ (x, τ) (CKN.basisVec i) * gradPair m ψ (x, τ) (CKN.basisVec i)

Integration by parts: one derivative of gradPair can be moved onto a second compactly supported test function.

theorem CIV.integral_partialLaplacian_mul_eq_neg_integral_gradPair_mul {m d : ℕ} {φ ψ : CKN.Vec m × ℝ → ℝ} {τ : ℝ} (hφ : ContDiff ℝ ↑⊤ fun (x : CKN.Vec m) => φ (x, τ)) (hψ : ContDiff ℝ ↑⊤ fun (x : CKN.Vec m) => ψ (x, τ)) (hφsupp : HasCompactSupport fun (x : CKN.Vec m) => φ (x, τ)) : ∫ (x : CKN.Vec m), partialLaplacian m d φ (x, τ) * ψ (x, τ) = -∫ (x : CKN.Vec m), ∑ i : Fin m, if ↑i < d then gradPair m φ (x, τ) (CKN.basisVec i) * gradPair m ψ (x, τ) (CKN.basisVec i) else 0

Integration by parts for the full truncated Laplacian: moving one derivative from partialLaplacian onto a compactly supported test function.

theorem CIV.integral_partialLaplacian_mul_symm {m d : ℕ} {φ ψ : CKN.Vec m × ℝ → ℝ} {τ : ℝ} (hφ : ContDiff ℝ ↑⊤ fun (x : CKN.Vec m) => φ (x, τ)) (hψ : ContDiff ℝ ↑⊤ fun (x : CKN.Vec m) => ψ (x, τ)) (hφsupp : HasCompactSupport fun (x : CKN.Vec m) => φ (x, τ)) (hψsupp : HasCompactSupport fun (x : CKN.Vec m) => ψ (x, τ)) : ∫ (x : CKN.Vec m), partialLaplacian m d φ (x, τ) * ψ (x, τ) = ∫ (x : CKN.Vec m), φ (x, τ) * partialLaplacian m d ψ (x, τ)

Symmetry of the truncated-Laplacian pairing: the bilinear form induced by partialLaplacian is symmetric on smooth compactly supported test functions.