The sharp isoperimetric inequality for sets of finite volume

Let E be a finite-dimensional real inner product space of dimension n ≥ 1 with its volume, and write ω_n = volume (ball 0 1) and P(s) for the perimeter of s in the whole space. Every null-measurable set s of finite positive volume satisfies the sharp isoperimetric inequality

P(s)^n ≥ n^n ω_n |s|^(n-1)

(MeasureTheory.NullMeasurableSet.finrank_pow_mul_volume_ball_mul_volume_pow_le_perimeter_pow), with no boundedness, connectedness or regularity hypothesis on s, and with P(s) finite or infinite (when n = 0 the inequality holds trivially). Equivalently n ω_n^(1/n) |s|^(1 - 1/n) ≤ P(s) (MeasureTheory.NullMeasurableSet.ofReal_mul_volume_real_rpow_mul_le_perimeter), which is also stated in real numbers when the perimeter is finite (MeasureTheory.NullMeasurableSet.mul_volume_real_rpow_mul_le_perimeter_toReal). In dimension n ≥ 2 the inequality holds for every set of finite volume, the volume-zero case being trivial (NullMeasurableSet.finrank_pow_mul_volume_ball_mul_volume_pow_le_perimeter_pow_of_two_le). Balls attain equality (TauCeti.perimeter_ball_pow), so the constant is sharp. Finite volume cannot be dropped: the complement of a ball has finite perimeter.

Strategy

Every set of finite volume is a limit, in measure and in perimeter, of regular superlevel sets {u > t} of compactly supported smooth functions (MeasureTheory.NullMeasurableSet.exists_smooth_perimeter_approximation), so it suffices to treat such sets. For these, w = (u - t) / √(‖∇u‖² + (u - t)²) is a smooth defining function of F = {u > t} whose gradient has norm one on the boundary {u = t} (ContDiff.exists_contDiff_setOf_pos_eq_setOf_lt). Near the boundary ‖∇w‖ lies within ε of one, and for small η > 0:

• the η / (1 + ε)-neighbourhood of G = {w ≥ η} lies in F, so the Brunn–Minkowski inequality bounds the volume of the shell S = {0 < w < η} = F \ G from below by n |G|^(1 - 1/n) ω_n^(1/n) η / (1 + ε);
• for a test vector field ψ equal to -∇w / ‖∇w‖ near the boundary, integration by parts against the clamped function max 0 (min w η) gives the calibration estimate (1 - ε) |S| ≤ ∫_S ‖∇w‖ ≤ η (∫_F div ψ + ∫_S |div ψ|) (ContDiff.setIntegral_norm_fderiv_le).

Dividing by η, letting η → 0 and then ε → 0 gives n ω_n^(1/n) |F|^(1 - 1/n) ≤ ∫_F div ψ, and the right-hand side is at most P(F) by the definition of the perimeter. No identification of the perimeter with surface measure or Minkowski content is used.

Main results

• MeasureTheory.NullMeasurableSet.finrank_pow_mul_volume_ball_mul_volume_pow_le_perimeter_pow: the sharp isoperimetric inequality n^n ω_n |s|^(n-1) ≤ P(s)^n in ℝ≥0∞.
• NullMeasurableSet.finrank_pow_mul_volume_ball_mul_volume_pow_le_perimeter_pow_of_two_le: the same inequality in dimension n ≥ 2 for every set of finite volume.
• MeasureTheory.NullMeasurableSet.ofReal_mul_volume_real_rpow_mul_le_perimeter: the equivalent form n ω_n^(1/n) |s|^(1 - 1/n) ≤ P(s) in ℝ≥0∞, with no hypothesis on the perimeter.
• MeasureTheory.NullMeasurableSet.mul_volume_real_rpow_mul_le_perimeter_toReal: its real form for sets of finite perimeter.
• ContDiff.ofReal_mul_volume_real_rpow_mul_le_perimeter_setOf_lt: the smooth case, for a regular superlevel set {u > t} of a compactly supported smooth function u with t > 0.

References

• F. Maggi, Sets of Finite Perimeter and Geometric Variational Problems, Cambridge University Press, 2012, Chapters 13 and 14, for the approximation by smooth sets and the isoperimetric inequality.
• R. J. Gardner, The Brunn–Minkowski inequality, Bull. Amer. Math. Soc. 39 (2002), 355–405, Section 5.

theorem ContDiff.ofReal_mul_volume_real_rpow_mul_le_perimeter_setOf_lt {E : Type u_1} [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) (hV : MeasureTheory.volume {x : E | t < u x} ≠ 0) : ENNReal.ofReal (↑(Module.finrank ℝ E) * MeasureTheory.volume.real (Metric.ball 0 1) ^ (↑(Module.finrank ℝ E))⁻¹ * MeasureTheory.volume.real {x : E | t < u x} ^ (1 - (↑(Module.finrank ℝ E))⁻¹)) ≤ TauCeti.perimeter MeasureTheory.volume ⊤ {x : E | t < u x}

The sharp isoperimetric inequality for regular superlevel sets. Let u be smooth and compactly supported, and let t > 0 be a regular value of u. If F = {u > t} has positive volume, then n ω_n ^ (1 / n) |F| ^ (1 - 1 / n) ≤ P(F), trivially so in dimension n = 0.

theorem MeasureTheory.NullMeasurableSet.ofReal_mul_volume_real_rpow_mul_le_perimeter {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E} (hs : NullMeasurableSet s volume) (hμs : volume s ≠ ⊤) (hs0 : volume s ≠ 0) : ENNReal.ofReal (↑(Module.finrank ℝ E) * volume.real (Metric.ball 0 1) ^ (↑(Module.finrank ℝ E))⁻¹ * volume.real s ^ (1 - (↑(Module.finrank ℝ E))⁻¹)) ≤ TauCeti.perimeter volume ⊤ s

The sharp isoperimetric inequality, extended-real form. In a Euclidean space of dimension n, every null-measurable set s of finite positive volume satisfies n ω_n ^ (1 / n) |s| ^ (1 - 1 / n) ≤ P(s), where ω_n = volume (ball 0 1) and P(s) is the perimeter of s in the whole space, finite or infinite. No boundedness or regularity is assumed, and the case n = 0 is trivial.

theorem MeasureTheory.NullMeasurableSet.mul_volume_real_rpow_mul_le_perimeter_toReal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E} (hs : NullMeasurableSet s volume) (hμs : volume s ≠ ⊤) (hs0 : volume s ≠ 0) (hP : TauCeti.perimeter volume ⊤ s ≠ ⊤) : ↑(Module.finrank ℝ E) * volume.real (Metric.ball 0 1) ^ (↑(Module.finrank ℝ E))⁻¹ * volume.real s ^ (1 - (↑(Module.finrank ℝ E))⁻¹) ≤ (TauCeti.perimeter volume ⊤ s).toReal

The sharp isoperimetric inequality, real-valued form. In a Euclidean space of dimension n, every null-measurable set s of finite positive volume and finite perimeter satisfies n ω_n ^ (1 / n) |s| ^ (1 - 1 / n) ≤ P(s), where ω_n = volume (ball 0 1) and P(s) is the perimeter of s in the whole space. No boundedness or regularity is assumed, and the case n = 0 is trivial.

theorem MeasureTheory.NullMeasurableSet.finrank_pow_mul_volume_ball_mul_volume_pow_le_perimeter_pow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E} (hs : NullMeasurableSet s volume) (hμs : volume s ≠ ⊤) (hs0 : volume s ≠ 0) : ↑(Module.finrank ℝ E) ^ Module.finrank ℝ E * volume (Metric.ball 0 1) * volume s ^ (Module.finrank ℝ E - 1) ≤ TauCeti.perimeter volume ⊤ s ^ Module.finrank ℝ E

The sharp isoperimetric inequality. In a Euclidean space of dimension n, every null-measurable set s of finite positive volume satisfies P(s)^n ≥ n^n ω_n |s|^(n-1), where ω_n = volume (ball 0 1) and P(s) is the perimeter of s in the whole space, finite or infinite. No boundedness or regularity is assumed, and the case n = 0 is trivial. Balls attain equality (TauCeti.perimeter_ball_pow).

theorem MeasureTheory.NullMeasurableSet.finrank_pow_mul_volume_ball_mul_volume_pow_le_perimeter_pow_of_two_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E} (hs : NullMeasurableSet s volume) (hμs : volume s ≠ ⊤) (hn : 2 ≤ Module.finrank ℝ E) : ↑(Module.finrank ℝ E) ^ Module.finrank ℝ E * volume (Metric.ball 0 1) * volume s ^ (Module.finrank ℝ E - 1) ≤ TauCeti.perimeter volume ⊤ s ^ Module.finrank ℝ E

The sharp isoperimetric inequality in dimension n ≥ 2. In a Euclidean space of dimension n ≥ 2, every null-measurable set s of finite volume satisfies P(s)^n ≥ n^n ω_n |s|^(n-1), where ω_n = volume (ball 0 1) and P(s) is the perimeter of s in the whole space, finite or infinite. Sets of volume zero satisfy it trivially, since then n^n ω_n |s|^(n-1) = 0.