mathlib documentation

data.nat.choose.central

Central binomial coefficients #

This file proves properties of the central binomial coefficients (that is, nat.choose (2 * n) n).

Main definition and results #

def nat.central_binom (n : ) :

The central binomial coefficient, nat.choose (2 * n) n.

Equations
@[simp]
theorem nat.choose_le_central_binom (r n : ) :

The central binomial coefficient is the largest binomial coefficient.

theorem nat.two_le_central_binom (n : ) (n_pos : 0 < n) :
theorem nat.succ_mul_central_binom_succ (n : ) :
(n + 1) * (n + 1).central_binom = 2 * (2 * n + 1) * n.central_binom

An inductive property of the central binomial coefficient.

theorem nat.four_pow_lt_mul_central_binom (n : ) (n_big : 4 n) :
4 ^ n < n * n.central_binom

An exponential lower bound on the central binomial coefficient. This bound is of interest because it appears in Tochiori's refinement of Erdős's proof of Bertrand's postulate.

theorem nat.four_pow_le_two_mul_self_mul_central_binom (n : ) (n_pos : 0 < n) :
4 ^ n 2 * n * n.central_binom

An exponential lower bound on the central binomial coefficient. This bound is weaker than four_pow_n_lt_n_mul_central_binom, but it is of historical interest because it appears in Erdős's proof of Bertrand's postulate.

A logarithmic upper bound on the multiplicity of a prime in the central binomial coefficient.

theorem nat.padic_val_nat_central_binom_of_large_le_one {p n : } (hp : nat.prime p) (p_large : 2 * n < p ^ 2) :

Sufficiently large primes appear only to multiplicity 0 or 1 in the central binomial coefficient.

theorem nat.padic_val_nat_central_binom_of_large_eq_zero {p n : } (hp : nat.prime p) (n_big : 2 < n) (p_le_n : p n) (big : 2 * n < 3 * p) :

Sufficiently large primes less than n do not appear in the factorisation of central_binom n.