English
If n > 2 and there is no prime in the interval (n, 2n], then the central binomial coefficient is bounded by (2n)^{√(2n)} · 4^{(2n)/3}.
Русский
Если n > 2 и в интервале (n, 2n] нет простого числа, то центральная биномиальная коэффициента удовлетворяет ограничению: C(2n, n) ≤ (2n)^{√(2n)} · 4^{(2n)/3}.
LaTeX
$$$\displaystyle \binom{2n}{n} \le (2n)^{\sqrt{2n}} \cdot 4^{\left\lfloor \frac{2n}{3} \right\rfloor}$, при условиях $2 < n$ и не существует простого $p$ с $n < p \le 2n$.$$
Lean4
/-- An upper bound on the central binomial coefficient used in the proof of Bertrand's postulate.
The bound splits the prime factors of `centralBinom n` into those
1. At most `sqrt (2 * n)`, which contribute at most `2 * n` for each such prime.
2. Between `sqrt (2 * n)` and `2 * n / 3`, which contribute at most `4^(2 * n / 3)` in total.
3. Between `2 * n / 3` and `n`, which do not exist.
4. Between `n` and `2 * n`, which would not exist in the case where Bertrand's postulate is false.
5. Above `2 * n`, which do not exist.
-/
theorem centralBinom_le_of_no_bertrand_prime (n : ℕ) (n_large : 2 < n)
(no_prime : ¬∃ p : ℕ, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n) :
centralBinom n ≤ (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) :=
by
have n_pos : 0 < n := (Nat.zero_le _).trans_lt n_large
have n2_pos : 1 ≤ 2 * n := mul_pos (zero_lt_two' ℕ) n_pos
let S := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
let f x := x ^ n.centralBinom.factorization x
have : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x :=
by
refine Finset.prod_filter_of_ne fun p _ h => ?_
contrapose! h; dsimp only [f]
rw [factorization_eq_zero_of_non_prime n.centralBinom h, _root_.pow_zero]
rw [centralBinom_factorization_small n n_large no_prime, ← this, ←
Finset.prod_filter_mul_prod_filter_not S (· ≤ sqrt (2 * n))]
apply mul_le_mul'
· refine (Finset.prod_le_prod' fun p _ => (?_ : f p ≤ 2 * n)).trans ?_
· exact pow_factorization_choose_le (mul_pos two_pos n_pos)
have : (Finset.Icc 1 (sqrt (2 * n))).card = sqrt (2 * n) := by rw [card_Icc, Nat.add_sub_cancel]
rw [Finset.prod_const]
refine pow_right_mono₀ n2_pos ((Finset.card_le_card fun x hx => ?_).trans this.le)
obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hx
exact Finset.mem_Icc.mpr ⟨(Finset.mem_filter.1 h1).2.one_lt.le, h2⟩
· refine le_trans ?_ (primorial_le_4_pow (2 * n / 3))
refine (Finset.prod_le_prod' fun p hp => (?_ : f p ≤ p)).trans ?_
· obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hp
refine (pow_right_mono₀ (Finset.mem_filter.1 h1).2.one_lt.le ?_).trans (pow_one p).le
exact Nat.factorization_choose_le_one (sqrt_lt'.mp <| not_le.1 h2)
refine Finset.prod_le_prod_of_subset_of_one_le' (Finset.filter_subset _ _) ?_
exact fun p hp _ => (Finset.mem_filter.1 hp).2.one_lt.le
