LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite epsilon nets of the Euclidean sphere

Statement

Let $d \geq 1$ be an integer and $0 < ϵ < 1$ . There is a finite set $N \subseteq S^{d - 1}$ such that every $u \in S^{d - 1}$ has some $v \in N$ with $∥ u - v ∥_{2} \leq ϵ$ , and $∣ N ∣ \leq (1 + 2 / ϵ)^{d} .$ Here $S^{d - 1} = {u \in R^{d} : ∥ u ∥_{2} = 1}$ by Euclidean spheres and closed balls as subspaces of $R^{n}$ . Such a set is called an $ϵ$ -net of the sphere.

Facts & Assumptions

Given: An integer $d \geq 1$ and $0 < ϵ < 1$ .

[F1]

The closed Euclidean ball and sphere are ${\overline{B}}_{2} (c, r) = {x : ∥ x - c ∥_{2} \leq r}$ and $S_{2} (c, r) = {x : ∥ x - c ∥_{2} = r}$ ; the unit sphere is $S^{d - 1} = S_{2} (0, 1)$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ ).

[F2]

$d_{2} (x, y) = ∥ x - y ∥_{2}$ is a metric, so it satisfies the triangle inequality ( $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it).

[F3]

Closed Euclidean balls are Jordan measurable, with $V_{1} (r) = 2 r$ and the stated slicing recursion for $V_{d} (r)$ (Closed Euclidean balls are Jordan measurable and their volumes satisfy the slicing recursion).

[F4]

An invertible linear map scales Jordan content by the absolute determinant; in particular $cont (r {\overline{B}}_{2} (0, 1)) = r^{d} cont ({\overline{B}}_{2} (0, 1))$ for $r > 0$ (A linear endomorphism of $R^{n}$ sends bounded Jordan sets to bounded Jordan sets and scales their content by the absolute determinant).

[F5]

Translation preserves Jordan content (Jordan inner content, outer content, measurability, and content are translation invariant).

[F6]

Jordan content is additive on finite disjoint families of bounded Jordan sets (Jordan content is finitely additive when the overlap has content zero).

[F7]

Jordan outer content is the infimum of volumes of finite rectangle covers, and the content of a Jordan set is its common inner/outer value (Jordan inner and outer content and Jordan measurable bounded sets in $R^{m}$ ).

[F8]

The natural numbers are unbounded in $R$ (Every complete ordered field is Archimedean).

[F9]

Every nonempty finite set of real numbers has a maximum (Every nonempty finite set of reals has a maximum and a minimum).

[F10]

For rational $α > 0$ , rational powers preserve order on positive bases, and $0^{α} = 0$ (Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ , Rational powers $a^{r}$ of a positive base).

[F11]

The Riemann integral is monotone and additive across a cut, and the integral of a constant $c$ on an interval $[a, b]$ is $c (b - a)$ (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ , The lower and upper Darboux integrals over a nondegenerate rectangle in $R^{m}$ ).

Proof

1.1givenF3F10F11algebra

Put $V_{d} = cont ({\overline{B}}_{2} (0, 1))$ . This number is finite by [F3] and positive by induction on $d$ : $V_{1} = 2$ , and for $d \geq 2$ set $α = (d - 1) / 2 > 0$ . On $[- 1 / 2, 1 / 2]$ , $1 - t^{2} \geq 3 / 4$ , so [F10] gives $(1 - t^{2})^{α} \geq (3 / 4)^{α} > 0$ ; on all of $[- 1, 1]$ this integrand is nonnegative. By [F11], splitting the integral at $- 1 / 2$ and $1 / 2$ and comparing the middle part with the constant $(3 / 4)^{α}$ shows $\int_{- 1}^{1} (1 - t^{2})^{α} d t \geq (3 / 4)^{α} > 0$ . The volume recursion [F3] then gives $V_{d} > 0$ from $V_{d - 1} > 0$ .

1.2givenF1F2

Let $E = {x_{1}, \dots, x_{N}} \subseteq S^{d - 1}$ have pairwise distances greater than $ϵ$ , and put $r = ϵ / 2$ . The closed balls ${\overline{B}}_{2} (x_{j}, r)$ are pairwise disjoint: a point in two of them would, by the triangle inequality [F2], put the corresponding centers at distance at most $2 r = ϵ$ , contrary to the separation. Each small ball lies in ${\overline{B}}_{2} (0, 1 + r)$ , since $∥ x_{j} ∥_{2} = 1$ and [F2] gives $∥ y ∥_{2} \leq ∥ y - x_{j} ∥_{2} + ∥ x_{j} ∥_{2} \leq r + 1$ .

2.1F4F5F6F7step 1.1step 1.2algebra

By scaling and translation invariance [F4, F5], every small ball in step 1.2 has content $r^{d} V_{d}$ and the large ball has content $(1 + r)^{d} V_{d}$ . Finite additivity [F6] and monotonicity of outer content from [F7] give $N r^{d} V_{d} \leq (1 + r)^{d} V_{d}$ . Step 1.1 gives $V_{d} > 0$ , so cancellation and $r = ϵ / 2$ yield $N \leq ((1 + r) / r)^{d} = (1 + 2 / ϵ)^{d}$ . This also holds when $E$ is empty, for which $N = 0$ .

3.1givenF1F8F9step 2.1choose

Choose an integer $M > (1 + 2 / ϵ)^{d}$ using [F8]. Let $K$ be the set of cardinalities of finite subsets of $S^{d - 1}$ whose distinct points are more than $ϵ$ apart. The first coordinate unit vector shows $K$ is nonempty, and step 2.1 shows every member of $K$ is at most $(1 + 2 / ϵ)^{d} < M$ . Thus $K$ is a nonempty subset of ${0, 1, \dots, M}$ ; [F9] gives a largest member $k \in K$ , attained by a finite set $N$ by the definition of $K$ .

4.1step 2.1step 3.1contradiction∎

If some $u \in S^{d - 1}$ were farther than $ϵ$ from every point of $N$ , adjoining $u$ would produce a finite set with pairwise distances greater than $ϵ$ and cardinality $k + 1$ , contradicting maximality in step 3.1. Thus $N$ is an $ϵ$ -net; step 2.1 gives its stated cardinality bound. This construction uses only a maximum in a finite set of possible cardinalities, not an axiom of choice.

Depends on

Used by

Dependency tree · two levels

81 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Philippe Rigollet and Jan-Christian Hütter, High-Dimensional Statistics: Lecture Notes, Chapter 1, §1.4, Lemma 1.18 (standard reference, not scraped)
John K. Hunter, Measure Theory, Jordan content and volume properties (standard reference, not scraped)