Integration by parts for space-time factors.

theorem CKN.instIsAddHaarMeasureProdVec3RealVolume : MeasureTheory.volume.IsAddHaarMeasure

theorem CKN.integral_mul_spatialPartial_eq_neg_spatialPartial_mul {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (hGcompact : HasCompactSupport G) (i : Fin 3) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), F z * spatialPartial (have this := G; this) i z = -∫ (z : Foundation.Parabolic.Vec3 × ℝ), spatialPartial (have this := F; this) i z * G z

theorem CKN.integral_mul_timePartial_eq_neg_timePartial_mul {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hG : ContDiff ℝ (↑⊤) G) (hGcompact : HasCompactSupport G) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), F z * timePartial (have this := G; this) z = -∫ (z : Foundation.Parabolic.Vec3 × ℝ), timePartial (have this := F; this) z * G z