The isoperimetric inequality #
A direct application of the Brunn–Minkowski inequality to a measurable set A
and an ε-ball yields the standard form of the isoperimetric inequality
relating volume A, the volume of the unit ball, and the volume of the
ε-thickening of A.
theorem
volume_ball_relation
{d : ℕ}
{ε : ℝ}
:
MeasureTheory.volume (Metric.ball 0 ε) ^ (↑d + 1)⁻¹ = MeasureTheory.volume (Metric.ball 0 1) ^ (↑d + 1)⁻¹ * ENNReal.ofReal ε
The volume of a Euclidean ball of radius ε raised to the 1/(d+1)-th power equals the
corresponding power for the unit ball times ε.
theorem
isoperimetric_inequality
{d : ℕ}
{ε : ℝ}
(hε : ε > 0)
{A : Set (EuclideanSpace ℝ (Fin (d + 1)))}
(hA_nonempty : A.Nonempty)
(hA_measurable : MeasurableSet A)
(hA_finite : MeasureTheory.volume A ≠ ⊤)
:
(↑d + 1) * MeasureTheory.volume A ^ (1 - (↑d + 1)⁻¹) * MeasureTheory.volume (Metric.ball 0 1) ^ (↑d + 1)⁻¹ ≤ (MeasureTheory.volume (A + Metric.ball 0 ε) - MeasureTheory.volume A) / ENNReal.ofReal ε
The isoperimetric inequality on Euclidean space, deduced from Brunn–Minkowski.