mathlib3 documentation

data.nat.choose.central

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 #

def nat.central_binom (n : ) :

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

Equations
@[simp]
theorem nat.choose_le_central_binom (r n : ) :

The central binomial coefficient is the largest binomial coefficient.

theorem nat.two_le_central_binom (n : ) (n_pos : 0 < n) :
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.

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.

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.

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