Central binomial coefficients #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

def nat.central_binom (n : ℕ) :

ℕ

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

Equations

n.central_binom = (2 * n).choose n

source

theorem nat.central_binom_eq_two_mul_choose (n : ℕ) :

n.central_binom = (2 * n).choose n

source

theorem nat.central_binom_pos (n : ℕ) :

0 < n.central_binom

source

theorem nat.central_binom_ne_zero (n : ℕ) :

n.central_binom ≠ 0

source

@[simp]

theorem nat.central_binom_zero :

0.central_binom = 1

source

theorem nat.choose_le_central_binom (r n : ℕ) :

(2 * n).choose r ≤ n.central_binom

The central binomial coefficient is the largest binomial coefficient.

source

theorem nat.two_le_central_binom (n : ℕ) (n_pos : 0 < n) :

2 ≤ n.central_binom

source

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.

source

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.

source

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.

source

theorem nat.two_dvd_central_binom_succ (n : ℕ) :

2 ∣ (n + 1).central_binom

source

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

2 ∣ n.central_binom

source

theorem nat.succ_dvd_central_binom (n : ℕ) :

n + 1 ∣ n.central_binom

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