The divergence theorem on a half-space of an inner product space

Let F be a finite-dimensional real inner product space of dimension n, let ν be a unit vector and c a real number. This file proves the divergence theorem on the open half-space H = {x | ⟪x, ν⟫ < c}, whose outward unit normal is ν and whose boundary is the hyperplane {x | ⟪x, ν⟫ = c} carrying the normalized (n - 1)-dimensional Hausdorff measure μHE[n - 1]. For a compactly supported C¹ vector field φ,

∫_H tr (Dφ) = ∫_{⟪x, ν⟫ = c} ⟪φ x, ν⟫ dμHE[n - 1].

The hyperplane is the image of the orthogonal complement (ℝ ∙ ν)ᗮ under the isometry y ↦ c • ν + y, so its Hausdorff measure is the image of the Lebesgue measure of that (n - 1)-dimensional inner product space (TauCeti.euclideanHausdorffMeasure_restrict_setOf_inner_eq, in TauCeti.Geometry.Euclidean.Volume.Measure). The divergence theorem is transported by a linear isometry F ≃ ℝ × (ℝ ∙ ν)ᗮ from its form on the coordinate half-space of the ℓ² product, TauCeti.setIntegral_normalHalfSpace_fderiv_apply.

Main results

• TauCeti.setIntegral_setOf_inner_lt_fderiv_apply: for a compactly supported C¹ function g and a direction v, ∫_H ∂_v g = ⟪v, ν⟫ ∫_{⟪x, ν⟫ = c} g dμHE[n - 1].
• TauCeti.setIntegral_setOf_inner_lt_trace_fderiv: the divergence theorem on H for compactly supported C¹ vector fields.

References

• L. C. Evans, Partial Differential Equations, Appendix C.2 (the Gauss–Green theorem).

theorem TauCeti.setIntegral_setOf_inner_lt_fderiv_apply {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ν : F} [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (hν : ‖ν‖ = 1) (c : ℝ) {g : F → ℝ} (hg : ContDiff ℝ 1 g) (hgc : HasCompactSupport g) (v : F) : ∫ (x : F) in {x : F | inner ℝ x ν < c}, (fderiv ℝ g x) v = inner ℝ v ν * ∫ (x : F) in {x : F | inner ℝ x ν = c}, g x ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ F - 1)

The divergence theorem on a half-space, directional form. For a unit vector ν, a compactly supported C¹ function g and a direction v, the integral of ∂_v g over the half-space {x | ⟪x, ν⟫ < c} is the integral of g over the boundary hyperplane against (n - 1)-dimensional Hausdorff measure, weighted by the normal component ⟪v, ν⟫ of v.

theorem TauCeti.setIntegral_setOf_inner_lt_trace_fderiv {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ν : F} [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] (hν : ‖ν‖ = 1) (c : ℝ) {φ : F → F} (hφ : ContDiff ℝ 1 φ) (hφc : HasCompactSupport φ) : ∫ (x : F) in {x : F | inner ℝ x ν < c}, (LinearMap.trace ℝ F) ↑(fderiv ℝ φ x) = ∫ (x : F) in {x : F | inner ℝ x ν = c}, inner ℝ (φ x) ν ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ F - 1)

The divergence theorem on a half-space. For a unit vector ν and a compactly supported C¹ vector field φ, the integral of the divergence tr (Dφ) over the half-space {x | ⟪x, ν⟫ < c} is the flux ∫ ⟪φ, ν⟫ of φ through the boundary hyperplane {x | ⟪x, ν⟫ = c} against (n - 1)-dimensional Hausdorff measure.