The perimeter of a ball

Let μ be an additive Haar measure on a finite-dimensional real inner product space E of dimension n, and write ω = μ (ball 0 1). A ball of radius r > 0 has perimeter

P(ball c r) = n ω r^(n-1) = (n / r) μ (ball c r)

in the whole space (TauCeti.perimeter_ball, TauCeti.perimeter_ball_eq_ofReal_div_mul). For μ the volume of EuclideanSpace ℝ (Fin n) this is the classical surface area n ω_n r^(n-1) of the sphere of radius r, where ω_n is the volume of the unit ball. The perimeter only sees a set up to null sets, so the closed ball has the same perimeter (TauCeti.perimeter_closedBall). In dimension n ≥ 1 balls satisfy P(ball c r)^n = n^n ω μ (ball c r)^(n-1) (TauCeti.perimeter_ball_pow): they attain equality in the isoperimetric inequality P(E)^n ≥ n^n ω μ E^(n-1), whose constant is fixed by this identity.

The perimeter is computed from its definition by duality. The test vector field x ↦ θ x • (x - c) / (r + δ), for a smooth bump θ equal to one on the ball and supported in the ball of radius r + δ, has norm at most one and constant divergence n / (r + δ) on the ball, which gives the lower bound as δ → 0. For the upper bound, the perimeter of the closed ball is at most its lower outer Minkowski content (TauCeti.perimeter_closure_le_liminf_measure_thickening_sdiff_div). The ε-neighbourhood of the closed ball is the open ball of radius r + ε, so this content is the derivative n r^(n-1) ω of r ↦ r^n ω.

Main results

• TauCeti.perimeter_ball: P(ball c r) = n r^(n-1) μ (ball 0 1) for r > 0.
• TauCeti.perimeter_ball_eq_ofReal_div_mul: P(ball c r) = (n / r) μ (ball c r).
• TauCeti.perimeter_closedBall: the same formula for closed balls.
• TauCeti.perimeter_ball_pow: P(ball c r)^n = n^n μ (ball 0 1) μ (ball c r)^(n-1).

References

• F. Maggi, Sets of Finite Perimeter and Geometric Variational Problems, Chapter 12.

theorem TauCeti.perimeter_ball {E : Type u_1} [NormedAddCommGroup E] {c : E} {r : ℝ} [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (hr : 0 < r) : perimeter μ ⊤ (Metric.ball c r) = ↑(Module.finrank ℝ E) * ENNReal.ofReal (r ^ (Module.finrank ℝ E - 1)) * μ (Metric.ball 0 1)

The perimeter of a ball. Against an additive Haar measure μ on a space of dimension n, a ball of radius r > 0 has perimeter n r^(n-1) μ (ball 0 1) in the whole space. For the volume of EuclideanSpace ℝ (Fin n) this is the surface area n ω_n r^(n-1) of the sphere of radius r.

theorem TauCeti.perimeter_ball_eq_ofReal_div_mul {E : Type u_1} [NormedAddCommGroup E] {c : E} {r : ℝ} [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] : perimeter μ ⊤ (Metric.ball c r) = ENNReal.ofReal (↑(Module.finrank ℝ E) / r) * μ (Metric.ball c r)

The perimeter of a ball, normalized by its volume. A ball of radius r has perimeter (n / r) μ (ball c r), where n is the dimension. For r ≤ 0 the ball is empty and both sides are 0.

theorem TauCeti.perimeter_closedBall {E : Type u_1} [NormedAddCommGroup E] {c : E} {r : ℝ} [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (hr : 0 < r) : perimeter μ ⊤ (Metric.closedBall c r) = ↑(Module.finrank ℝ E) * ENNReal.ofReal (r ^ (Module.finrank ℝ E - 1)) * μ (Metric.ball 0 1)

The perimeter of a closed ball. A closed ball of radius r > 0 has the same perimeter n r^(n-1) μ (ball 0 1) as the open ball, since they differ by a null set.

theorem TauCeti.perimeter_ball_pow {E : Type u_1} [NormedAddCommGroup E] {c : E} {r : ℝ} [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (hn : Module.finrank ℝ E ≠ 0) (hr : 0 < r) : perimeter μ ⊤ (Metric.ball c r) ^ Module.finrank ℝ E = ↑(Module.finrank ℝ E) ^ Module.finrank ℝ E * μ (Metric.ball 0 1) * μ (Metric.ball c r) ^ (Module.finrank ℝ E - 1)

Balls are isoperimetric equality cases. In dimension n ≥ 1, a ball of radius r > 0 satisfies P(ball c r)^n = n^n μ (ball 0 1) μ (ball c r)^(n-1), equality in the isoperimetric inequality P(E)^n ≥ n^n μ (ball 0 1) μ E^(n-1).