Calibrating the shells of a smooth defining function

Let w be a smooth real function on a finite-dimensional real inner product space whose derivative does not vanish on its zero level, so that F = {w > 0} is a set with smooth boundary {w = 0}. The unit normal field -∇w / ‖∇w‖ calibrates w near that boundary: if {w ≥ -δ} is compact, a cutoff of this field is an admissible test vector field ψ, with ‖ψ‖ ≤ 1 everywhere and Dw (ψ) = -‖Dw‖ on a band {|w| ≤ η} (ContDiff.exists_testFunction_fderiv_apply_eq_neg_norm).

Integrating by parts against the clamped function max 0 (min w η) then controls the gradient of w on the shell S = {0 < w < η} by the divergence of ψ:

∫_S ‖Dw‖ ≤ η (∫_F div ψ + ∫_S |div ψ|)

(ContDiff.setIntegral_norm_fderiv_le). Since ∫_F div ψ is at most the perimeter of F, this bounds the volume of thin shells next to a smooth boundary by the perimeter. It drives the sharp isoperimetric inequality for smooth sets and the comparison of the outer Minkowski content of a smooth set with its perimeter.

References

• F. Maggi, Sets of Finite Perimeter and Geometric Variational Problems, Cambridge University Press, 2012, Chapter 13.

theorem ContDiff.exists_testFunction_fderiv_apply_eq_neg_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {w : E → ℝ} (hw : ContDiff ℝ (↑⊤) w) {δ : ℝ} (hδ : 0 < δ) (hK : IsCompact {x : E | -δ ≤ w x}) (hreg : ∀ (x : E), w x = 0 → fderiv ℝ w x ≠ 0) : ∃ η > 0, ∃ (ψ : TestFunction ⊤ E ⊤), (∀ (x : E), ‖ψ x‖ ≤ 1) ∧ ∀ (x : E), |w x| ≤ η → (fderiv ℝ w x) (ψ x) = -‖fderiv ℝ w x‖

A smooth function w whose derivative does not vanish on its zero level, with {w ≥ -δ} compact, admits an admissible test vector field equal to -∇w / ‖∇w‖ near the zero level. Its derivative pairing with w there is -‖Dw‖.

theorem ContDiff.setIntegral_norm_fderiv_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {w : E → ℝ} (hw : ContDiff ℝ 1 w) {η : ℝ} (hη : 0 < η) (ψ : TestFunction ⊤ E ⊤) (hψ : ∀ (x : E), w x ∈ Set.Ioo 0 η → (fderiv ℝ w x) (ψ x) = -‖fderiv ℝ w x‖) : ∫ (x : E) in w ⁻¹' Set.Ioo 0 η, ‖fderiv ℝ w x‖ ≤ η * ((∫ (x : E), (TestFunction.divergenceCLM ψ) x * {x : E | 0 < w x}.indicator 1 x) + ∫ (x : E) in w ⁻¹' Set.Ioo 0 η, |(TestFunction.divergenceCLM ψ) x|)

The calibration estimate. If a test vector field ψ satisfies Dw (ψ) = -‖Dw‖ on the shell S = {0 < w < η}, as -∇w / ‖∇w‖ does, then ∫_S ‖Dw‖ ≤ η (∫_{w > 0} div ψ + ∫_S |div ψ|).