Compact-test integration by parts for the Laplacian

Evaluation of the first Fréchet derivative in a fixed direction commutes with differentiation.

Two integrations by parts in one direction, with a compactly supported test.

theorem LiebThirring.fderiv_directional_fderiv {f : Position → ℝ} (hf : ContDiff ℝ 2 f) (x u v : Position) : (fderiv ℝ (fun (z : Position) => (fderiv ℝ f z) v) x) u = ((fderiv ℝ (fderiv ℝ f) x) u) v

Evaluation of the first Fréchet derivative in a fixed direction commutes with differentiation.

theorem LiebThirring.integral_mul_hessian_eq_integral_hessian_mul {u f : Position → ℝ} (hu : ContDiff ℝ 2 u) (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) (v : Position) : ∫ (x : Position), u x * ((fderiv ℝ (fderiv ℝ f) x) v) v = ∫ (x : Position), ((fderiv ℝ (fderiv ℝ u) x) v) v * f x

Two integrations by parts in one direction, with a compactly supported test.

theorem LiebThirring.integral_mul_laplacian_eq_integral_laplacian_mul {u f : Position → ℝ} (hu : ContDiff ℝ 2 u) (hf : ContDiff ℝ 2 f) (hfc : HasCompactSupport f) : ∫ (x : Position), u x * Laplacian.laplacian f x = ∫ (x : Position), Laplacian.laplacian u x * f x

The Mathlib Laplacian is self-adjoint against compactly supported C² tests.