# 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 #

• 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.

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

Instances For
@[simp]
theorem Nat.choose_le_centralBinom (r : ) (n : ) :
Nat.choose (2 * n) r

The central binomial coefficient is the largest binomial coefficient.

theorem Nat.two_le_centralBinom (n : ) (n_pos : 0 < n) :
theorem Nat.succ_mul_centralBinom_succ (n : ) :
(n + 1) * Nat.centralBinom (n + 1) = 2 * (2 * n + 1) *

An inductive property of the central binomial coefficient.

theorem Nat.four_pow_lt_mul_centralBinom (n : ) (n_big : 4 n) :
4 ^ 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 < n4 ^ n 2 * 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.succ_dvd_centralBinom (n : ) :
n + 1

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