noncomputable def SphericalCap.sphereVolume (n : ℕ) : MeasureTheory.Measure ↑(Metric.sphere 0 1)

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

theorem SphericalCap.sphereVolume_univ_ne_top (n : ℕ) : (sphereVolume n) Set.univ ≠ ⊤

The total $(n-1)$-Hausdorff surface measure of the sphere $S^{n-1}$ is finite.

noncomputable def SphericalCap.normalizedSphereMeasure {n : ℕ} (A : Set ↑(Metric.sphere 0 1)) : ℝ

The uniform probability measure on $S^{n-1}$, defined by normalizing the $(n-1)$-Hausdorff surface measure: $\mu(A) = \operatorname{vol}(A) / \operatorname{vol}(S^{n-1})$.

theorem SphericalCap.normalizedSphereMeasure_subset_mono {n : ℕ} {A B : Set ↑(Metric.sphere 0 1)} (h : A ⊆ B) : normalizedSphereMeasure A ≤ normalizedSphereMeasure B

The normalized sphere measure is monotone with respect to set inclusion.

theorem SphericalCap.normalizedSphereMeasure_union_le {n : ℕ} (A B : Set ↑(Metric.sphere 0 1)) : normalizedSphereMeasure (A ∪ B) ≤ normalizedSphereMeasure A + normalizedSphereMeasure B

Subadditivity (union bound) of the normalized sphere measure: $\mu(A \cup B) \le \mu(A) + \mu(B)$.

noncomputable def SphericalCap.sphericalCapMeasure (n : ℕ) (ε : ℝ) : ℝ

The normalized measure of the spherical cap $\{x \in S^{n-1} \mid x_1 \ge \varepsilon\}$, i.e. $\mathbb{P}_{x \sim S^{n-1}}(x_1 \ge \varepsilon)$ (with the convention that the value is $0$ when $n = 0$).

theorem SphericalCap.sphericalCapMeasure_eq_zero_of_gt_one (n : ℕ) (ε : ℝ) (hε : ε > 1) : sphericalCapMeasure n ε = 0

For $\varepsilon > 1$ the cap $\{x \in S^{n-1} \mid x_1 \ge \varepsilon\}$ is empty, hence has measure $0$.

theorem SphericalCap.sphericalCapMeasure_le_case1 (n : ℕ) (ε : ℝ) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1 / √2) : sphericalCapMeasure n ε ≤ √(1 - ε ^ 2) ^ n

Spherical cap bound, small-$\varepsilon$ regime ($0 \le \varepsilon \le 1/\sqrt{2}$): $\mathbb{P}(x_1 \ge \varepsilon) \le (1 - \varepsilon^{2})^{n/2}$.

theorem SphericalCap.sphericalCapMeasure_le_case2 (n : ℕ) (ε : ℝ) (hε_lb : 1 / √2 ≤ ε) (hε_ub : ε ≤ 1) : sphericalCapMeasure n ε ≤ (1 / (2 * ε)) ^ n

Spherical cap bound, large-$\varepsilon$ regime ($1/\sqrt{2} \le \varepsilon \le 1$): $\mathbb{P}(x_1 \ge \varepsilon) \le \big(1/(2\varepsilon)\big)^{n}$.

theorem SphericalCap.sqrt_one_sub_sq_le_exp (ε : ℝ) : √(1 - ε ^ 2) ≤ Real.exp (-(ε ^ 2 / 2))

Real analysis lemma: $\sqrt{1 - \varepsilon^{2}} \le \exp(-\varepsilon^{2}/2)$, obtained from $1 - x \le e^{-x}$ and the identity $\sqrt{e^{-t}} = e^{-t/2}$.

theorem SphericalCap.inv_two_mul_le_exp (ε : ℝ) (hε_lb : 1 / √2 ≤ ε) (hε_ub : ε ≤ 1) : 1 / (2 * ε) ≤ Real.exp (-(ε ^ 2 / 2))

Real analysis lemma: for $1/\sqrt{2} \le \varepsilon \le 1$, $1/(2\varepsilon) \le \exp(-\varepsilon^{2}/2)$.

theorem SphericalCap.pow_le_exp_of_le {r ε : ℝ} {n : ℕ} (hr : 0 ≤ r) (h : r ≤ Real.exp (-(ε ^ 2 / 2))) : r ^ n ≤ Real.exp (-(↑n * ε ^ 2 / 2))

Raising the bound $r \le e^{-\varepsilon^{2}/2}$ to the $n$-th power yields $r^{n} \le \exp(-n \varepsilon^{2}/2)$.

theorem SphericalCap.spherical_cap_bound (n : ℕ) (ε : ℝ) (hε : 0 ≤ ε) : sphericalCapMeasure n ε ≤ Real.exp (-(↑n * ε ^ 2 / 2))

Spherical cap concentration (Theorem 9.4.11). For a uniformly random unit vector $x \sim S^{n-1}$ and $\varepsilon \ge 0$, $\mathbb{P}(x_1 \ge \varepsilon) \le \exp(-n \varepsilon^{2}/2)$.

theorem SphericalCap.sphereVolume_pos_of_normalizedSphereMeasure_pos {n : ℕ} {A : Set ↑(Metric.sphere 0 1)} (h : normalizedSphereMeasure A > 0) : (sphereVolume n) Set.univ ≠ 0

Contrapositive helper: if the normalized measure of some set $A$ is positive, then the total surface volume of $S^{n-1}$ is nonzero (i.e. the sphere is genuinely $(n-1)$-dimensional).

theorem SphericalCap.normalizedSphereMeasure_compl {n : ℕ} (A : Set ↑(Metric.sphere 0 1)) (hA : MeasurableSet A) (hpos : (sphereVolume n) Set.univ ≠ 0) : normalizedSphereMeasure Aᶜ = 1 - normalizedSphereMeasure A

Probability complement: $\mu(A^c) = 1 - \mu(A)$ for the normalized sphere measure, provided the total surface volume is nonzero.

theorem SphericalCap.normalizedSphereMeasure_nonempty_of_pos {n : ℕ} (A : Set ↑(Metric.sphere 0 1)) (h : normalizedSphereMeasure A > 0) : A.Nonempty

A set of positive normalized sphere measure is nonempty.

theorem SphericalCap.sphere_thickening_complement_bound {n : ℕ} (A : Set ↑(Metric.sphere 0 1)) (hA : normalizedSphereMeasure A ≥ 1 / 2) (t : ℝ) (ht : 0 ≤ t) : 1 - normalizedSphereMeasure (Metric.cthickening t A) ≤ sphericalCapMeasure n (t / √2)

Key intermediate step in the concentration of measure on $S^{n-1}$: if $\mu(A) \ge 1/2$, then $1 - \mu(A_t) \le \mathbb{P}\!\big(x_1 \ge t/\sqrt{2}\big)$ for every $t \ge 0$, obtained from Lévy's isoperimetric inequality.

theorem SphericalCap.sphere_concentration {n : ℕ} (A : Set ↑(Metric.sphere 0 1)) (hA : normalizedSphereMeasure A ≥ 1 / 2) (t : ℝ) (ht : 0 ≤ t) : normalizedSphereMeasure (Metric.cthickening t A) ≥ 1 - Real.exp (-(↑n * t ^ 2 / 4))

Concentration of measure on the sphere (Corollary 9.4.12). If $\mu(A) \ge 1/2$ then $\mu(A_t) \ge 1 - \exp(-n t^{2}/4)$ for every $t \ge 0$.

theorem SphericalCap.sphere_median_exists {n : ℕ} (f : ↑(Metric.sphere 0 1) → ℝ) : ∃ (m : ℝ), normalizedSphereMeasure {x : ↑(Metric.sphere 0 1) | f x ≤ m} ≥ 1 / 2 ∧ normalizedSphereMeasure {x : ↑(Metric.sphere 0 1) | f x ≥ m} ≥ 1 / 2

Existence of a median for any function $f : S^{n-1} \to \mathbb{R}$: there is some $m \in \mathbb{R}$ such that both $\{f \le m\}$ and $\{f \ge m\}$ have normalized sphere measure at least $1/2$.

theorem SphericalCap.sphere_lipschitz_sublevel_bound {n : ℕ} (f : ↑(Metric.sphere 0 1) → ℝ) (hf_lip : LipschitzWith 1 f) (m t : ℝ) (ht : 0 ≤ t) (hm : normalizedSphereMeasure {x : ↑(Metric.sphere 0 1) | f x ≤ m} ≥ 1 / 2) : normalizedSphereMeasure {x : ↑(Metric.sphere 0 1) | f x > m + t} ≤ 1 - normalizedSphereMeasure (Metric.cthickening t {x : ↑(Metric.sphere 0 1) | f x ≤ m})

For a $1$-Lipschitz function $f : S^{n-1} \to \mathbb{R}$ with median bound $\mu(f \le m) \ge 1/2$, the upper tail $\{f > m + t\}$ has measure at most $1 - \mu(\text{thickening}_t \{f \le m\})$. This is the geometric link between Lipschitz tails and isoperimetric thickening.

theorem SphericalCap.sphere_lipschitz_upper_tail {n : ℕ} (f : ↑(Metric.sphere 0 1) → ℝ) (hf_lip : LipschitzWith 1 f) (m : ℝ) (hm : normalizedSphereMeasure {x : ↑(Metric.sphere 0 1) | f x ≤ m} ≥ 1 / 2) (t : ℝ) (ht : 0 ≤ t) : normalizedSphereMeasure {x : ↑(Metric.sphere 0 1) | f x > m + t} ≤ Real.exp (-(↑n * t ^ 2 / 4))

One-sided concentration for $1$-Lipschitz functions on the sphere: if $m$ is a median of $f$ then $\mu(f > m + t) \le \exp(-n t^{2}/4)$ for all $t \ge 0$.

theorem SphericalCap.sphere_lipschitz_concentration {n : ℕ} (f : ↑(Metric.sphere 0 1) → ℝ) (hf_lip : LipschitzWith 1 f) : ∃ (m : ℝ), ∀ (t : ℝ), 0 ≤ t → normalizedSphereMeasure {x : ↑(Metric.sphere 0 1) | |f x - m| > t} ≤ 2 * Real.exp (-(↑n * t ^ 2 / 4))

Concentration of $1$-Lipschitz functions on the sphere (Corollary 9.4.14). For any $1$-Lipschitz $f : S^{n-1} \to \mathbb{R}$ there exists a median $m \in \mathbb{R}$ such that $\mu(|f - m| > t) \le 2 \exp(-n t^{2}/4)$ for every $t \ge 0$.