The relative isoperimetric inequality in a ball

Let E be a finite-dimensional real inner product space of dimension n ≥ 2 with an additive Haar measure μ, and write ω = μ(B(0, 1)). This file proves the relative isoperimetric inequality: for every ball B = B(c, r) and every set s null-measurable in B,

min (μ(s ∩ B), μ(B \ s)) ^ (1 - 1/n) ≤ 2 ^ (n + 1) ω ^ (-1/n) P(s; B).

The constant does not depend on the radius, so the inequality is invariant under scaling, and the perimeter may be taken in any open set containing the ball. Neither finite perimeter nor any regularity of s is assumed. This is the estimate that turns perimeter bounds into the density estimates of the boundary structure theory of sets of finite perimeter.

It is the indicator case of the localized Poincaré–Wirtinger inequality for functions of bounded variation,

∫_A |u - ⨍_S u| ≤ ω ^ (1 - 1/n) (diam Ω) ^ n / μ(S) μ(A) ^ (1/n) |Du|(Ω)

(TauCeti.setLIntegral_enorm_sub_setAverage_le_mul_measure_rpow_mul_totalVariationOn_of_convex). For an indicator, testing it on A = s ∩ B or A = B \ s, whichever the indicator deviates from its mean on by at least 1/2, and dividing by μ(A) ^ (1/n) gives the relative isoperimetric inequality.

Main results

• TauCeti.min_measure_inter_measure_sdiff_rpow_le_perimeter: the relative isoperimetric inequality in a ball.

References

• L. Ambrosio, N. Fusco, D. Pallara, Functions of Bounded Variation and Free Discontinuity Problems, Remark 3.50.
• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, §5.6.2.
• F. Maggi, Sets of Finite Perimeter and Geometric Variational Problems, Proposition 12.37.

theorem TauCeti.min_measure_inter_measure_sdiff_rpow_le_perimeter {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {Ω : TopologicalSpace.Opens E} (hn : 2 ≤ Module.finrank ℝ E) {s : Set E} {c : E} {r : ℝ} (hs : MeasureTheory.NullMeasurableSet s (μ.restrict (Metric.ball c r))) (hΩ : Metric.ball c r ⊆ ↑Ω) : min (μ (s ∩ Metric.ball c r)) (μ (Metric.ball c r \ s)) ^ (1 - (↑(Module.finrank ℝ E))⁻¹) ≤ ENNReal.ofReal (2 ^ (Module.finrank ℝ E + 1) / μ.real (Metric.ball 0 1) ^ (↑(Module.finrank ℝ E))⁻¹) * perimeter μ Ω s

The relative isoperimetric inequality in a ball. Let E have dimension n ≥ 2 and let ω = μ(B(0, 1)). If the ball B = B(c, r) lies in the open set Ω and s is null-measurable in B, then min (μ(s ∩ B), μ(B \ s)) ^ (1 - 1/n) ≤ 2 ^ (n + 1) ω ^ (-1/n) P(s; Ω). The constant does not depend on the radius, and the perimeter may be infinite.