Integration by parts for spatial derivatives

The weak-form integration by parts identity ∫ u ∂_i φ = -∫ ∂_i u φ for smooth compactly supported functions on Vec3.

theorem CKN.integral_mul_spatialDeriv_eq_neg_integral_spatialDeriv_mul {u φ : Foundation.Parabolic.Vec3 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (i : Fin 3) : ∫ (x : Foundation.Parabolic.Vec3), u x * spatialDeriv φ i x = -∫ (x : Foundation.Parabolic.Vec3), spatialDeriv u i x * φ x

Integration by parts for a single spatial derivative: ∫ u (∂_i φ) = -∫ (∂_i u) φ for smooth u, φ with compactly supported φ.