Smooth integration by parts for the shear fields.

theorem CKN.integral_mul_fderiv_eq_neg_fderiv_mul_of_contDiff_compact_right {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [OpensMeasurableSpace E] [FiniteDimensional ℝ E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {f g : E → ℝ} {v : E} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : ∫ (x : E), f x * (fderiv ℝ g x) v ∂μ = -∫ (x : E), (fderiv ℝ f x) v * g x ∂μ