The divergence theorem on a half-space of a Euclidean product

For a compactly supported C¹ function g on ℝ × E (with the Euclidean norm), the derivative in the normal direction e₁ integrates over Ioi a ×ˢ E to minus the boundary integral over {a} × E (TauCeti.integral_prod_fderiv_normal), and the derivative in a tangential direction (0, w) integrates to zero (TauCeti.integral_prod_fderiv_tangent).

theorem TauCeti.integral_prod_fderiv_normal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {g : WithLp 2 (ℝ × E) → ℝ} (hg : ContDiff ℝ 1 g) (hgc : HasCompactSupport g) (a : ℝ) : ∫ (z : ℝ × E), (fderiv ℝ g (WithLp.toLp 2 z)) (WithLp.toLp 2 (1, 0)) ∂(MeasureTheory.volume.restrict (Set.Ioi a)).prod MeasureTheory.volume = -∫ (y : E), g (WithLp.toLp 2 (a, y))

The normal part of the divergence theorem on a half-space: for a compactly supported C¹ function g on ℝ × E, the integral of ∂_{e₁} g over Ioi a ×ˢ E is minus the integral of g over the boundary slice {a} × E, by the fundamental theorem of calculus on each normal line.

theorem TauCeti.integral_prod_fderiv_tangent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {g : WithLp 2 (ℝ × E) → ℝ} (hg : ContDiff ℝ 1 g) (hgc : HasCompactSupport g) (a : ℝ) (w : E) : ∫ (z : ℝ × E), (fderiv ℝ g (WithLp.toLp 2 z)) (WithLp.toLp 2 (0, w)) ∂(MeasureTheory.volume.restrict (Set.Ioi a)).prod MeasureTheory.volume = 0

The tangential part of the divergence theorem on a half-space: the integral over Ioi a ×ˢ E of a derivative of a compactly supported C¹ function g along a direction (0, w) tangent to the slices vanishes, since it integrates to zero on each slice {t} × E.