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.centralBinom_strictMono :

StrictMono centralBinom

source

theorem Nat.two_le_centralBinom (n : ℕ) (n_pos : 0 < n) :

2 ≤ n.centralBinom

source

theorem Nat.centralBinom_le_four_pow (n : ℕ) :

n.centralBinom ≤ 4 ^ n

source

theorem Nat.centralBinom_lt_four_pow {n : ℕ} (h : n ≠ 0) :

n.centralBinom < 4 ^ n

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][tochiori_bertrand].

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.four_pow_le_two_mul_add_one_mul_centralBinom (n : ℕ) :

4 ^ n ≤ (2 * n + 1) * n.centralBinom

source

@[deprecated Nat.four_pow_le_two_mul_add_one_mul_centralBinom (since := "2026-09-13")]

theorem Nat.four_pow_le_two_mul_add_one_mul_central_binom (n : ℕ) :