exists_large_sphere_aux — Mathlib

English

For all n,d, ((d^n)/((n·(d−1)^2)+1)) ≤ rothNumberNat((2d−1)^n).

Русский

Для всех n,d выполняется неравенство d^n/(n(d−1)^2+1) ≤ rothNumberNat((2d−1)^n).

LaTeX

$$$ \\frac{d^n}{n (d-1)^2 + 1} \\leq \\operatorname{rothNumberNat}((2d-1)^n) $$$

Lean4

theorem exists_large_sphere_aux (n d : ℕ) :
    ∃ k ∈ range (n * (d - 1) ^ 2 + 1), (↑(d ^ n) / ((n * (d - 1) ^ 2 :) + 1) : ℝ) ≤ #(sphere n d k) :=
  by
  refine exists_le_card_fiber_of_nsmul_le_card_of_maps_to (fun x hx => ?_) nonempty_range_add_one ?_
  · rw [mem_range, Nat.lt_succ_iff]
    exact sum_sq_le_of_mem_box hx
  · rw [card_range, nsmul_eq_mul, mul_div_assoc', cast_add_one, mul_div_cancel_left₀, card_box]
    exact (cast_add_one_pos _).ne'

Похожие утверждения