Smooth half-space normal Green identity

Proved

HunterPDE.Shared.integral_mul_smooth_normal

by Mazecto · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

integration-by-partspdetrace

For smooth compactly supported $f,\psi$ on $\mathbb R^{m+1}$ ,

\int_{\mathbb R^{m+1}_+}\partial_{m+1}f\,\psi=-\int_{\mathbb R^{m+1}_+}f\,\partial_{m+1}\psi-\int_{\mathbb R^m}f(x',0)\psi(x',0)\,dx'.

This includes $m=0$ and retains the nonzero boundary contribution. One-dimensional integration by parts on normal rays and Fubini prove it. It is the classical ingredient in extending Green's formula by Sobolev density.

Preamble

import Definitions.Def_HunterPDE_Compactness_HalfSpace
import Definitions.Def_HunterPDE_Shared_WeakDeriv
import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
open MeasureTheory HunterPDE.Compactness HunterPDE.Shared Filter
open scoped ENNReal Topology ContDiff
set_option autoImplicit false

Formal statement

theorem HunterPDE.Shared.integral_mul_smooth_normal {m : ℕ}
    (f ψ : EuclideanSpace ℝ (Fin (m + 1)) → ℝ)
    (hf : IsTestFunction Set.univ f) (hψ : IsTestFunction Set.univ ψ) :
    (∫ x in upperHalfSpace m, partialDeriv f (Fin.last m) x * ψ x) =
      -(∫ x in upperHalfSpace m, f x * multiDeriv ψ (Pi.single (Fin.last m) 1) x) -
        ∫ x', f (boundaryPoint x') * ψ (boundaryPoint x') := by sorry

Source

J. K. Hunter, Notes on Partial Differential Equations, revised 6/18/2014, https://www.math.ucdavis.edu/~hunter/pdes/ch3.pdf, Theorems 3.42 and 3.44, printed pp. 72–73. Auxiliary ingredient for the normal Green identity, not an explicit numbered theorem in the source.

View graph