@[reducible, inline]

abbrev SphereArrangement.R3 : Type

Three-dimensional Euclidean space $\mathbb{R}^3$ used for the sphere-cutting bound.

structure SphereArrangement.Sphere3 : Type

A sphere in $\mathbb{R}^3$ specified by a center and a strictly positive radius.

• center : R3
• radius : ℝ
• radius_pos : 0 < self.radius

def SphereArrangement.Sphere3.toSet (S : Sphere3) : Set R3

The underlying point set of a sphere: $\{x \in \mathbb{R}^3 : \|x - c\| = r\}$.

def SphereArrangement.sphereUnion {n : ℕ} (spheres : Fin n → Sphere3) : Set R3

The union $\bigcup_i S_i$ of a finite family of spheres in $\mathbb{R}^3$.

noncomputable def SphereArrangement.numComponentsComplement {n : ℕ} (spheres : Fin n → Sphere3) : ℕ

Number of connected components of the complement of $\bigcup_i S_i$ in $\mathbb{R}^3$.

theorem SphereArrangement.one_sphere_components (S : Fin 1 → Sphere3) : numComponentsComplement S = 2

A single sphere divides $\mathbb{R}^3$ into exactly $2$ connected components (interior and exterior).

theorem SphereArrangement.sphere_addition_components {m : ℕ} (spheres : Fin (m + 1) → Sphere3) (hm : 1 ≤ m) : ↑(numComponentsComplement spheres) ≤ ↑(numComponentsComplement fun (i : Fin m) => spheres i.castSucc) + (↑m * (↑m - 1) + 2)

Inductive step: adding one more sphere to an arrangement of $m \ge 1$ spheres can increase the number of complementary components by at most $m(m-1) + 2$.

theorem SphereArrangement.sphere_arrangement_components_le_cube {n : ℕ} (hn : 2 ≤ n) (spheres : Fin n → Sphere3) : numComponentsComplement spheres ≤ n ^ 3

Lemma 6.2.14: any arrangement of $n \ge 2$ spheres in $\mathbb{R}^3$ cuts the space into at most $n^3$ connected components.