# mathlibdocumentation

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 #

• 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.
• succ_dvd_central_binom: The result that n+1 ∣ n.central_binom, ensuring that the explicit definition of the Catalan numbers is integer-valued.
def nat.central_binom (n : ) :

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

Equations
theorem nat.central_binom_pos (n : ) :
@[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 <

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 nat.four_pow_lt_mul_central_binom, but it is of historical interest because it appears in Erdős's proof of Bertrand's postulate.

theorem nat.two_dvd_central_binom_of_one_le {n : } (h : 0 < n) :

A crucial lemma to ensure that Catalan numbers can be defined via their explicit formula catalan n = n.central_binom / (n + 1).