Perimeter and outer Minkowski content

Let μ be an additive Haar measure on a finite-dimensional real inner product space E. For every set s and every open set Ω, the perimeter of the closure of s in Ω is at most the lower outer Minkowski content of s in Ω:

P(closure s; Ω) ≤ liminf_{ε → 0⁺} μ((s_ε \ closure s) ∩ Ω) / ε,

where s_ε = Metric.thickening ε s is the open ε-neighbourhood of s (TauCeti.perimeter_closure_le_liminf_measure_thickening_sdiff_div). No measurability, finite measure or regularity hypothesis on s is needed.

For a compact set K, the closed neighbourhoods K + t • closedBall 0 1 are the outer parallel sets of K. If their volume has a right derivative D at t = 0, then P(K) ≤ D (IsCompact.perimeter_le_of_hasDerivWithinAt). For convex bodies of positive volume this is one half of the identification of the perimeter with the first variation of parallel volume.

The first bound is proved by approximating the indicator of the closure of s by Lipschitz functions. Mathlib's ε-thickened indicator thickenedIndicator of s is ε⁻¹-Lipschitz, equals one on the closure of s and vanishes off s_ε. It attains its maximum on the closure of s and its minimum off s_ε, so its derivative vanishes there, and its total variation in Ω is at most ε⁻¹ μ((s_ε \ closure s) ∩ Ω). The thickened indicators converge to the indicator of the closure of s locally in L¹, since the shells s_ε \ closure s decrease to the empty set, and lower semicontinuity of the total variation concludes.

For sets with smooth boundary the outer Minkowski content is the perimeter. If u is smooth and compactly supported and t > 0 is a regular value of u, the closed superlevel set s = {u ≥ t} satisfies |s_ε \ s| / ε → P(s) as ε → 0⁺ (ContDiff.tendsto_volume_thickening_sdiff_div). The lower bound is the general one above. For the upper bound, write s = {w ≥ 0} for a smooth defining function w with ‖Dw‖ = 1 on the boundary (ContDiff.exists_contDiff_setOf_pos_eq_setOf_lt). Since ‖Dw‖ ≤ 1 + δ near the boundary, s_ε \ s lies in the shell {-(1 + δ) ε < w < 0} for small ε, and the calibration estimate for -w bounds the volume of that shell by (1 + δ) ε P(s) / (1 - 2 δ) (ContDiff.setIntegral_norm_fderiv_le).

Main results

• TauCeti.perimeter_closure_le_liminf_measure_thickening_sdiff_div: the perimeter of the closure is at most the lower outer Minkowski content.
• IsCompact.tendsto_measure_cthickening_sdiff_div: if the parallel volume of a compact set has right derivative D at zero, its outer shells have volume D t + o(t).
• IsCompact.perimeter_le_of_hasDerivWithinAt: the perimeter of a compact set is at most the right derivative at zero of the volume of its outer parallel sets.
• ContDiff.tendsto_volume_thickening_sdiff_div: the outer Minkowski content of a regular closed superlevel set of a compactly supported smooth function is its perimeter.

References

• F. Maggi, Sets of Finite Perimeter and Geometric Variational Problems, Chapter 12.
• L. Ambrosio, N. Fusco, D. Pallara, Functions of Bounded Variation and Free Discontinuity Problems, Section 2.13, for Minkowski content.

theorem TauCeti.perimeter_closure_le_liminf_measure_thickening_sdiff_div {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (Ω : TopologicalSpace.Opens E) (s : Set E) : perimeter μ Ω (closure s) ≤ Filter.liminf (fun (ε : ℝ) => μ (Metric.thickening ε s \ closure s ∩ ↑Ω) / ENNReal.ofReal ε) (nhdsWithin 0 (Set.Ioi 0))

The perimeter is at most the lower outer Minkowski content. For every set s and every open set Ω, the perimeter of the closure of s in Ω is at most liminf_{ε → 0⁺} μ((s_ε \ closure s) ∩ Ω) / ε, where s_ε is the open ε-thickening of s. No measurability, finite-measure or regularity hypothesis on s is needed.

theorem IsCompact.tendsto_measure_cthickening_sdiff_div {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {K : Set E} (hK : IsCompact K) {D : ℝ} (hD : HasDerivWithinAt (fun (t : ℝ) => μ.real (K + t • Metric.closedBall 0 1)) D (Set.Ioi 0) 0) : Filter.Tendsto (fun (t : ℝ) => μ (Metric.cthickening t K \ K) / ENNReal.ofReal t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (ENNReal.ofReal D))

If the volume of the outer parallel sets K + t • closedBall 0 1 of a compact set K has right derivative D at t = 0, then the shells cthickening t K \ K have volume D t + o(t) as t → 0⁺.

theorem IsCompact.perimeter_le_of_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {K : Set E} (hK : IsCompact K) {D : ℝ} (hD : HasDerivWithinAt (fun (t : ℝ) => μ.real (K + t • Metric.closedBall 0 1)) D (Set.Ioi 0) 0) : TauCeti.perimeter μ ⊤ K ≤ ENNReal.ofReal D

The perimeter of a compact set is at most the first variation of its parallel volume. If the volume of the outer parallel sets K + t • closedBall 0 1 of a compact set K has right derivative D at t = 0, then P(K) ≤ D.

Regular superlevel sets of smooth functions

theorem ContDiff.tendsto_volume_thickening_sdiff_div {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u : E → ℝ} (hu : ContDiff ℝ (↑⊤) u) (huc : HasCompactSupport u) {t : ℝ} (ht : 0 < t) (hreg : ∀ (x : E), u x = t → fderiv ℝ u x ≠ 0) : Filter.Tendsto (fun (r : ℝ) => MeasureTheory.volume (Metric.thickening r {x : E | t ≤ u x} \ {x : E | t ≤ u x}) / ENNReal.ofReal r) (nhdsWithin 0 (Set.Ioi 0)) (nhds (TauCeti.perimeter MeasureTheory.volume ⊤ {x : E | t ≤ u x}))

Outer Minkowski content of a regular superlevel set. Let u be smooth and compactly supported, and let t > 0 be a regular value of u. The closed superlevel set s = {u ≥ t} has outer Minkowski content equal to its perimeter: |s_r \ s| / r → P(s) as r → 0⁺, where s_r is the open r-neighbourhood of s.