Documentation

Mathlib.Data.Nat.Choose.Central

Central binomial coefficients #

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

Main definition and results #

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 :
    Nat.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).