English
If Bertrand’s postulate fails, the prime factors of the central binomial coefficient are bounded by 2n/3+1.
Русский
Если постулат Бернанди не выполняется, простые делители центральной биномиальной коэффициента ограничены 2n/3+1.
LaTeX
$$centralBinom(n) = ∏ p ∈ [0, 2n/3] p^{factorization(p)}$$
Lean4
/-- A lemma that tells us that, in the case where Bertrand's postulate does not hold, the prime
factorization of the central binomial coefficient only has factors at most `2 * n / 3 + 1`.
-/
theorem centralBinom_factorization_small (n : ℕ) (n_large : 2 < n) (no_prime : ¬∃ p : ℕ, p.Prime ∧ n < p ∧ p ≤ 2 * n) :
centralBinom n = ∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ (centralBinom n).factorization p :=
by
refine (Eq.trans ?_ n.prod_pow_factorization_centralBinom).symm
apply Finset.prod_subset
· exact Finset.range_subset_range.2 (add_le_add_right (Nat.div_le_self _ _) _)
intro x hx h2x
rw [Finset.mem_range, Nat.lt_succ_iff] at hx h2x
rw [not_le, div_lt_iff_lt_mul three_pos, mul_comm x] at h2x
replace no_prime := not_exists.mp no_prime x
rw [← and_assoc, not_and', not_and_or, not_lt] at no_prime
rcases no_prime hx with h | h
· rw [factorization_eq_zero_of_non_prime n.centralBinom h, Nat.pow_zero]
· rw [factorization_centralBinom_of_two_mul_self_lt_three_mul n_large h h2x, Nat.pow_zero]
