Central binomial coefficients #

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

Main definition and results #

• Nat.centralBinom: the central binomial coefficient, (2 * n).choose n.
• Nat.succ_mul_centralBinom_succ: the inductive relationship between successive central binomial coefficients.
• Nat.four_pow_lt_mul_centralBinom: an exponential lower bound on the central binomial coefficient.
• succ_dvd_centralBinom: The result that n+1 ∣ n.centralBinom, ensuring that the explicit definition of the Catalan numbers is integer-valued.

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

Equations
• n.centralBinom = (2 * n).choose n
Instances For
theorem Nat.centralBinom_eq_two_mul_choose (n : ) :
n.centralBinom = (2 * n).choose n
theorem Nat.centralBinom_pos (n : ) :
0 < n.centralBinom
theorem Nat.centralBinom_ne_zero (n : ) :
n.centralBinom 0
@[simp]
theorem Nat.choose_le_centralBinom (r : ) (n : ) :
(2 * n).choose r n.centralBinom

The central binomial coefficient is the largest binomial coefficient.

theorem Nat.two_le_centralBinom (n : ) (n_pos : 0 < n) :
2 n.centralBinom
theorem Nat.succ_mul_centralBinom_succ (n : ) :
(n + 1) * (n + 1).centralBinom = 2 * (2 * n + 1) * n.centralBinom

An inductive property of the central binomial coefficient.

theorem Nat.four_pow_lt_mul_centralBinom (n : ) (n_big : 4 n) :
4 ^ n < n * n.centralBinom

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_centralBinom (n : ) :
0 < n4 ^ n 2 * n * n.centralBinom

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

theorem Nat.two_dvd_centralBinom_succ (n : ) :
2 (n + 1).centralBinom
theorem Nat.two_dvd_centralBinom_of_one_le {n : } (h : 0 < n) :
2 n.centralBinom
theorem Nat.succ_dvd_centralBinom (n : ) :
n + 1 n.centralBinom

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