Vanishing integrals of compactly supported derivatives

Space-time boundary terms in eq:carleman-commutator of the Escauriaza–Seregin–Šverák manuscript vanish for smooth compactly supported scalar fields.

theorem CKN.integral_spatialPartial_eq_zero {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hfc : HasCompactSupport f) (i : Fin 3) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), spatialPartial f i z = 0

The integral of a compactly supported smooth spatial derivative is zero.

theorem CKN.integral_timePartial_eq_zero {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hfc : HasCompactSupport f) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), timePartial f z = 0

The integral of a compactly supported smooth time derivative is zero.