Central binomial coefficients #

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

Main definition and results #

nat.central_binom: the central binomial coefficient, (2 * n).choose n.
nat.succ_mul_central_binom_succ: the inductive relationship between successive central binomial coefficients.
nat.four_pow_lt_mul_central_binom: an exponential lower bound on the central binomial coefficient.

source

def nat.central_binom (n : ℕ) :

ℕ

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

Equations

n.central_binom = (2 * n).choose n

source

theorem nat.central_binom_eq_two_mul_choose (n : ℕ) :

n.central_binom = (2 * n).choose n

source

theorem nat.central_binom_pos (n : ℕ) :

0 < n.central_binom

source

theorem nat.central_binom_ne_zero (n : ℕ) :

n.central_binom ≠ 0

source

@[simp]

theorem nat.central_binom_zero :

0.central_binom = 1

source

theorem nat.choose_le_central_binom (r n : ℕ) :

(2 * n).choose r ≤ n.central_binom

The central binomial coefficient is the largest binomial coefficient.

source

theorem nat.two_le_central_binom (n : ℕ) (n_pos : 0 < n) :

2 ≤ n.central_binom

source

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.

source

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.

source

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.