English
The cardinality of Behrend's sphere is bounded above by Roth numbers: # (sphere n d k) ≤ rothNumberNat((2d−1)^n).
Русский
Мощность сферы Behrend ограничена числом rothNumberNat((2d−1)^n).
LaTeX
$$$ \\#(\\text{sphere } n\\, d\\, k) \\leq \\operatorname{rothNumberNat}((2d-1)^n) $$$
Lean4
theorem card_sphere_le_rothNumberNat (n d k : ℕ) : #(sphere n d k) ≤ rothNumberNat ((2 * d - 1) ^ n) :=
by
cases n
· dsimp; refine (card_le_univ _).trans_eq ?_; rfl
cases d
· simp
apply threeAPFree_image_sphere.le_rothNumberNat _ _ (card_image_of_injOn _)
· simp only [mem_image, and_imp, forall_exists_index, sphere, mem_filter]
rintro _ x hx _ rfl
exact (map_le_of_mem_box hx).trans_lt sum_lt
apply map_injOn.mono fun x => ?_
simp only [mem_coe, sphere, mem_filter, mem_box, and_imp, two_mul]
exact fun h _ i => (h i).trans_le le_self_add
