Smooth approximation of sets of finite volume in perimeter

A Lebesgue-measurable set of finite volume admits bounded open approximations with smooth boundary, converging both in symmetric-difference measure and in perimeter on the whole space. The set need not be bounded, and finite perimeter is not assumed: the perimeter convergence is extended-valued, so the construction also covers infinite perimeter. Finite volume cannot be replaced by finite perimeter here, since the complement of a ball has finite perimeter but no bounded set approximates it in measure. The approximations are positive regular superlevels of compactly supported smooth functions. Thus their smoothness is witnessed by defining functions, rather than assumed as a predicate.

The first step is a truncation: cutting a set of finite measure by the closed half-spaces bounding a large cube does not increase its perimeter (TauCeti.perimeter_inter_biInter_halfSpace_le), so the set is the limit of bounded subsets whose perimeters converge to its own (MeasureTheory.NullMeasurableSet.exists_isBounded_perimeter_approximation). A bounded set is then approximated as follows. Mollify the indicator, choose regular levels in intervals expanding to (0, 1), and use ContDiff.exists_mem_Ioo_isCompact_closure_perimeter_le for perimeter control. The quantitative threshold estimate Measure.measure_symmDiff_setOf_lt_indicator_le controls the volume error uniformly in each interval. Lower semicontinuity then supplies the reverse perimeter bound. Null modifications of the original set require no choice of a Borel representative.

Main results

• MeasureTheory.NullMeasurableSet.exists_smooth_perimeter_approximation: approximation of a set of finite measure by bounded open sets with smooth boundary, in measure and in perimeter.

References

• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, §5.2.2.
• F. Maggi, Sets of Finite Perimeter and Geometric Variational Problems, Chapter 13.

theorem MeasureTheory.NullMeasurableSet.exists_smooth_perimeter_approximation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : Measure E} [μ.IsAddHaarMeasure] {s : Set E} (hs : NullMeasurableSet s μ) (hμs : μ s ≠ ⊤) : ∃ (u : ℕ → E → ℝ) (t : ℕ → ℝ), (∀ (n : ℕ), ContDiff ℝ (↑⊤) (u n) ∧ HasCompactSupport (u n) ∧ t n ∈ Set.Ioo 0 1 ∧ (∀ (x : E), u n x = t n → Function.Surjective ⇑(fderiv ℝ (u n) x)) ∧ IsCompact (closure {x : E | t n < u n x}) ∧ frontier {x : E | t n < u n x} = {x : E | u n x = t n} ∧ TauCeti.perimeter μ ⊤ {x : E | t n < u n x} < ⊤) ∧ Filter.Tendsto (fun (n : ℕ) => μ (symmDiff {x : E | t n < u n x} s)) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n : ℕ) => TauCeti.perimeter μ ⊤ {x : E | t n < u n x}) Filter.atTop (nhds (TauCeti.perimeter μ ⊤ s))

Smooth approximation of sets of finite volume. Every null-measurable set of finite measure is approximated in volume and perimeter by bounded open sets with smooth boundary. The sets are positive regular superlevels of compactly supported smooth functions and have finite perimeter; their frontiers are the corresponding regular levels. Perimeters are extended-valued, including when the original set has infinite perimeter, and the set itself need not be bounded.