English
The maximum possible size of a 1-separated set contained in the ball of radius 2 is finite; this is the key quantity controlling Besicovitch covering.
Русский
Максимальная возможная емкость 1-разделённого множества внутри шара радиуса 2 конечна; это ключевая величина в покрытии Бесицковича.
LaTeX
$$$$\\text{multiplicity }E := sSup\\{N\\mid \\exists s:\\ Finset E, s.card = N \\wedge (\\forall c\\in s, \\|c\\|\\le 2) \\wedge \\forall c\\in s, \\forall d\\in s, c\\neq d \\Rightarrow 1 \\le \\|c-d\\|\\}$$$$
Lean4
/-- The maximum cardinality of a `1`-separated set in the ball of radius `2`. This is also the
optimal number of families in the Besicovitch covering theorem. -/
def multiplicity (E : Type*) [NormedAddCommGroup E] :=
sSup {N | ∃ s : Finset E, s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}
