def SurfaceArea.unitBall (n : ℕ) : Set (EuclideanSpace ℝ (Fin n))

def SurfaceArea.minkowskiThickening {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) (ε : ℝ) : Set (EuclideanSpace ℝ (Fin n))

noncomputable def SurfaceArea.surfaceArea {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) : ℝ

theorem SurfaceArea.minkowskiThickening_unitBall_eq {ε : ℝ} {n : ℕ} (hε : 0 ≤ ε) : minkowskiThickening (unitBall n) ε = Metric.closedBall 0 (1 + ε)

theorem SurfaceArea.minkowskiThickening_unitBall_eq_smul {ε : ℝ} {n : ℕ} (hε : 0 ≤ ε) : minkowskiThickening (unitBall n) ε = (1 + ε) • unitBall n

theorem SurfaceArea.volume_minkowskiThickening_unitBall {ε : ℝ} {n : ℕ} (hε : 0 ≤ ε) : (MeasureTheory.volume (minkowskiThickening (unitBall n) ε)).toReal = (1 + ε) ^ n * (MeasureTheory.volume (unitBall n)).toReal

theorem SurfaceArea.surfaceArea_unitBall_eq {n : ℕ} (_hn : 2 ≤ n) (_hVB_pos : 0 < (MeasureTheory.volume (unitBall n)).toReal) : surfaceArea (unitBall n) = ↑n * (MeasureTheory.volume (unitBall n)).toReal

theorem SurfaceArea.surfaceArea_lower_bound {n : ℕ} (hn : 2 ≤ n) (K : Set (EuclideanSpace ℝ (Fin n))) (hK_convex : Convex ℝ K) (hK_compact : IsCompact K) (hK_interior : (interior K).Nonempty) (hK_meas : MeasurableSet K) (hVK_pos : 0 < (MeasureTheory.volume K).toReal) (hSK_pos : 0 < surfaceArea K) (hVB_pos : 0 < (MeasureTheory.volume (unitBall n)).toReal) : surfaceArea K ≥ ↑n * (MeasureTheory.volume K).toReal ^ ((↑n - 1) / ↑n) * (MeasureTheory.volume (unitBall n)).toReal ^ (1 / ↑n)

theorem SurfaceArea.isoperimetric_inequality {n : ℕ} (hn : 2 ≤ n) (K : Set (EuclideanSpace ℝ (Fin n))) (hK_convex : Convex ℝ K) (hK_compact : IsCompact K) (hK_interior : (interior K).Nonempty) (hK_meas : MeasurableSet K) (hVK_pos : 0 < (MeasureTheory.volume K).toReal) (hSK_pos : 0 < surfaceArea K) : ((MeasureTheory.volume K).toReal / (MeasureTheory.volume (unitBall n)).toReal) ^ (1 / ↑n) ≤ (surfaceArea K / surfaceArea (unitBall n)) ^ (1 / (↑n - 1))