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.

def Nat.centralBinom (n : ℕ) : ℕ

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

Equations

• Nat.centralBinom n = Nat.choose (2 * n) n

theorem Nat.centralBinom_eq_two_mul_choose (n : ℕ) : Nat.centralBinom n = Nat.choose (2 * n) n

theorem Nat.centralBinom_pos (n : ℕ) : 0 < Nat.centralBinom n

theorem Nat.centralBinom_ne_zero (n : ℕ) : Nat.centralBinom n ≠ 0

@[simp]

theorem Nat.centralBinom_zero : Nat.centralBinom 0 = 1

theorem Nat.choose_le_centralBinom (r : ℕ) (n : ℕ) : Nat.choose (2 * n) r ≤ Nat.centralBinom n

The central binomial coefficient is the largest binomial coefficient.

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

theorem Nat.succ_mul_centralBinom_succ (n : ℕ) : (n + 1) * Nat.centralBinom (n + 1) = 2 * (2 * n + 1) * Nat.centralBinom n

An inductive property of the central binomial coefficient.

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

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 < n → 4 ^ n ≤ 2 * n * Nat.centralBinom n

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 ∣ Nat.centralBinom (n + 1)

theorem Nat.two_dvd_centralBinom_of_one_le {n : ℕ} (h : 0 < n) : 2 ∣ Nat.centralBinom n

theorem Nat.succ_dvd_centralBinom (n : ℕ) : n + 1 ∣ Nat.centralBinom n

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