@[reducible, inline]

abbrev LevyIsoperimetric.UnitSphere (n : ℕ) : Type

The unit sphere $S^{n-1} \subseteq \mathbb{R}^n$, viewed as a subtype of $\mathbb{R}^n$ consisting of vectors of norm $1$.

def LevyIsoperimetric.IsSphericalCap {n : ℕ} (B : Set (UnitSphere n)) : Prop

A subset $B \subseteq S^{n-1}$ is a spherical cap if it has the form $\{x \in S^{n-1} \mid \langle x, v \rangle \ge c\}$ for some unit vector $v$ and some threshold $c \in \mathbb{R}$.

noncomputable def LevyIsoperimetric.sphereHausdorffMeasure (n : ℕ) : MeasureTheory.Measure (UnitSphere n)

The $(n-1)$-dimensional Hausdorff measure on the unit sphere $S^{n-1}$, used as the natural surface-area measure on the sphere.

theorem levy_isoperimetric_sphere (n : ℕ) (hn : 2 ≤ n) (A B : Set (LevyIsoperimetric.UnitSphere n)) (hB : LevyIsoperimetric.IsSphericalCap B) (hA_meas : MeasurableSet A) (hB_meas : MeasurableSet B) (hvol : (LevyIsoperimetric.sphereHausdorffMeasure n) A = (LevyIsoperimetric.sphereHausdorffMeasure n) B) (t : ℝ) (ht : 0 ≤ t) : (LevyIsoperimetric.sphereHausdorffMeasure n) (Metric.cthickening t A) ≥ (LevyIsoperimetric.sphereHausdorffMeasure n) (Metric.cthickening t B)

Lévy's isoperimetric inequality on the sphere (Theorem 9.4.10). Among all measurable subsets of the unit sphere $S^{n-1}$ with a fixed surface measure, spherical caps minimize the measure of the $t$-thickening: if $B$ is a spherical cap and $\mu(A) = \mu(B)$, then $\mu(A_t) \ge \mu(B_t)$ for every $t \ge 0$.