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.