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
πŸ”Έ coverage
def Nat.centralBinom (n : β„•) :
β„•

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

Instances For
    source
    πŸ“ coverage
    theorem Nat.centralBinom_eq_two_mul_choose (n : β„•) :
    n.centralBinom = (2 * n).choose n
    source
    πŸ“ coverage
    theorem Nat.centralBinom_pos (n : β„•) :
    0 < n.centralBinom
    source
    theorem Nat.centralBinom_ne_zero (n : β„•) :
    n.centralBinom β‰  0
    source
    πŸ“ coverage
    @[simp]
    theorem Nat.centralBinom_zero :
    centralBinom 0 = 1
    source
    πŸ“ coverage
    theorem Nat.choose_le_centralBinom (r n : β„•) :
    (2 * n).choose r ≀ n.centralBinom

    The central binomial coefficient is the largest binomial coefficient.

    source
    πŸ“ coverage
    theorem Nat.two_le_centralBinom (n : β„•) (n_pos : 0 < n) :
    2 ≀ n.centralBinom
    source
    πŸ“ coverage
    theorem Nat.centralBinom_le_four_pow (n : β„•) :
    n.centralBinom ≀ 4 ^ n
    source
    πŸ“ coverage
    theorem Nat.centralBinom_lt_four_pow {n : β„•} (h : n β‰  0) :
    n.centralBinom < 4 ^ n
    source
    πŸ“ coverage
    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
    πŸ“ coverage
    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
    πŸ“ coverage
    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
    πŸ“ coverage
    theorem Nat.two_dvd_centralBinom_succ (n : β„•) :
    2 ∣ (n + 1).centralBinom
    source
    πŸ“ coverage
    theorem Nat.two_dvd_centralBinom_of_one_le {n : β„•} (h : 0 < n) :
    2 ∣ n.centralBinom
    source
    πŸ“ coverage
    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).