Quantitative selection of regular superlevel sets

Every interval of levels of a smooth scalar function contains a regular value whose superlevel set has perimeter at most the total variation divided by the interval's length. For a compactly supported function and a positive interval, the selected superlevel set has compact closure, and its frontier is precisely the regular level set. These are the regular-value and perimeter estimates used when approximating sets of finite perimeter by bounded open sets with smooth boundary.

The selection combines the scalar BV coarea formula with the Morse--Sard theorem from TauCeti.Analysis.Calculus.Sard.OutermostStratum and Mathlib's first-moment method MeasureTheory.exists_notMem_null_le_laverage. No identification of perimeter with surface measure is asserted here.

References

• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, §5.2.2.

theorem ContDiff.exists_mem_Ioo_surjective_fderiv_perimeter_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → ℝ} {Ω : TopologicalSpace.Opens E} {a b : ℝ} (hu : ContDiff ℝ (↑⊤) u) (hab : a < b) : ∃ t ∈ Set.Ioo a b, (∀ (x : E), u x = t → Function.Surjective ⇑(fderiv ℝ u x)) ∧ TauCeti.perimeter μ Ω {x : E | t < u x} ≤ TauCeti.totalVariationOn μ Ω u / ENNReal.ofReal (b - a)

A smooth function has a regular value in every nonempty interval such that the perimeter of its superlevel set is at most its variation divided by the interval's length. The estimate also holds when the variation is infinite.

theorem ContDiff.exists_mem_Ioo_isCompact_closure_perimeter_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → ℝ} {Ω : TopologicalSpace.Opens E} {a b : ℝ} (hu : ContDiff ℝ (↑⊤) u) (hc : HasCompactSupport u) (ha : 0 ≤ a) (hab : a < b) : ∃ t ∈ Set.Ioo a b, (∀ (x : E), u x = t → Function.Surjective ⇑(fderiv ℝ u x)) ∧ IsCompact (closure {x : E | t < u x}) ∧ frontier {x : E | t < u x} = {x : E | u x = t} ∧ TauCeti.perimeter μ Ω {x : E | t < u x} ≤ TauCeti.totalVariationOn μ Ω u / ENNReal.ofReal (b - a)

For a compactly supported smooth function, a positive interval contains a regular value whose strict superlevel set has compact closure and the quantitative perimeter bound. Its frontier is the corresponding regular level set.