@[reducible, inline]

abbrev DecomposingCoverings.E3 : Type

Three-dimensional Euclidean space $\mathbb{R}^3$, the ambient space for the Mani-Levitska–Pach problem on coverings by unit balls.

def DecomposingCoverings.coveringSet {ι : Type u_1} (center : ι → E3) (x : E3) : Set ι

Indices of the unit balls that cover a point $x \in \mathbb{R}^3$: $\{i : x \in B(\text{center}_i, 1)\}$.

structure DecomposingCoverings.IsKFoldCovering {ι : Type u_1} (center : ι → E3) (k : ℕ) : Prop

IsKFoldCovering center k records that a family of unit balls with centres center is a locally finite $k$-fold covering of $\mathbb{R}^3$: every point is covered at least $k$ times and only by finitely many balls.

• cover (x : E3) : k ≤ (coveringSet center x).ncard
• locallyFinite (x : E3) : (coveringSet center x).Finite

noncomputable def DecomposingCoverings.mult {ι : Type u_1} (center : ι → E3) (x : E3) : ℕ

Multiplicity at $x$: the number of unit balls of the family covering $x$.

theorem DecomposingCoverings.proper_2coloring_exists (ι : Type u_1) (center : ι → E3) (k : ℕ) (hk : 2 ≤ k) (hcov : IsKFoldCovering center k) (h_mult_bound : ∀ (x : E3), ↑(mult center x) < 2 ^ (↑k / 3)) : ∃ (A : Set ι), (∀ (x : E3), ∃ i ∈ coveringSet center x, i ∈ A) ∧ ∀ (x : E3), ∃ j ∈ coveringSet center x, j ∉ A

Axiomatic statement underlying the Mani-Levitska–Pach theorem: if every point of $\mathbb{R}^3$ is covered fewer than $2^{k/3}$ times, then the family admits a proper $2$-colouring, i.e. a partition into two classes each of which still covers $\mathbb{R}^3$.