English
For natural numbers n and d there exists an index k such that the Behrend sphere sphere(n,d,k) has cardinality at least a specified real bound (d^n)/(n d^2).
Русский
Для натуральных чис n и d существует индекс k, такой что сфера Бера Hend sphere(n,d,k) имеет кардиналность не меньше заданного вещественного нижнего предела (d^n)/(n d^2).
LaTeX
$$$$ \exists k, \left( \frac{d^n}{n d^2} : \mathbb{R} \right) \le \#(\mathrm{sphere}(n,d,k)). $$$$
Lean4
theorem exists_large_sphere (n d : ℕ) : ∃ k, ((d ^ n :) / (n * d ^ 2 :) : ℝ) ≤ #(sphere n d k) :=
by
obtain ⟨k, -, hk⟩ := exists_large_sphere_aux n d
refine ⟨k, ?_⟩
obtain rfl | hn := n.eq_zero_or_pos
· simp
obtain rfl | hd := d.eq_zero_or_pos
· simp
refine (div_le_div_of_nonneg_left ?_ ?_ ?_).trans hk
· exact cast_nonneg _
· exact cast_add_one_pos _
simp only [← le_sub_iff_add_le', cast_mul, ← mul_sub, cast_pow, cast_sub hd, sub_sq, one_pow, cast_one, mul_one,
sub_add, sub_sub_self]
apply one_le_mul_of_one_le_of_one_le
· rwa [one_le_cast]
rw [_root_.le_sub_iff_add_le]
norm_num
exact one_le_cast.2 hd
