# 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.

source
def Nat.centralBinom (n : ℕ) :
ℕ

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

Equations

- n.centralBinom = (2 * n).choose n

Instances For

source
theorem Nat.centralBinom_eq_two_mul_choose (n : ℕ) :
n.centralBinom = (2 * n).choose n
source
theorem Nat.centralBinom_pos (n : ℕ) :
0 < n.centralBinom
source
theorem Nat.centralBinom_ne_zero (n : ℕ) :
n.centralBinom ≠ 0
source
@[simp]
theorem Nat.centralBinom_zero :
centralBinom 0 = 1
source
theorem Nat.choose_le_centralBinom (r n : ℕ) :
(2 * n).choose r ≤ n.centralBinom

The central binomial coefficient is the largest binomial coefficient.

source
theorem Nat.two_le_centralBinom (n : ℕ) (n_pos : 0 < n) :
2 ≤ n.centralBinom
source
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.

source
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.

source
theorem Nat.four_pow_le_two_mul_self_mul_centralBinom (n : ℕ) :
0 < n → 4 ^ 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.

source
theorem Nat.two_dvd_centralBinom_succ (n : ℕ) :
2 ∣ (n + 1).centralBinom
source
theorem Nat.two_dvd_centralBinom_of_one_le {n : ℕ} (h : 0 < n) :
2 ∣ n.centralBinom
source
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)`.