Nat.succ_dvd_centralBinom
theorem Nat.succ_dvd_centralBinom : ∀ (n : ℕ), n + 1 ∣ n.centralBinom
This theorem states that for any natural number `n`, `(n + 1)` is a divisor of the central binomial coefficient of `n`. In other words, when the central binomial coefficient `n.centralBinom` is divided by `(n + 1)`, the remainder is always zero. This is a key lemma for defining Catalan numbers using their explicit formula `catalan n = n.centralBinom / (n + 1)`.
More concisely: For all natural numbers n, (n + 1) divides the central binomial coefficient n.centralBinom.
|
Nat.choose_le_centralBinom
theorem Nat.choose_le_centralBinom : ∀ (r n : ℕ), (2 * n).choose r ≤ n.centralBinom
This theorem states that for any two natural numbers 'r' and 'n', the binomial coefficient of '2n choose r' is less than or equal to the central binomial coefficient of 'n'. In other words, any binomial coefficient involving '2n' and 'r' is always less than or equal to the central binomial coefficient of 'n'. The central binomial coefficient here refers to the binomial coefficient at the middle of the nth row in Pascal's triangle, which is always the largest in its row.
More concisely: For all natural numbers r and n, the binomial coefficient $\binom{2n}{r} \leq \binom{n}{n/2}$ where $\binom{n}{n/2}$ is the central binomial coefficient of the nth row in Pascal's triangle.
|
Nat.succ_mul_centralBinom_succ
theorem Nat.succ_mul_centralBinom_succ : ∀ (n : ℕ), (n + 1) * (n + 1).centralBinom = 2 * (2 * n + 1) * n.centralBinom
This theorem asserts a specific inductive property of the central binomial coefficient. For any natural number `n`, it states that the product of `n + 1` and the central binomial coefficient of `n + 1` is equal to twice the product of `2n + 1` and the central binomial coefficient of `n`. In mathematical notation, for all natural numbers `n`, we have `(n + 1) * binom((n + 1) + (n + 1), (n + 1)) = 2 * (2n + 1) * binom(n + n, n)`.
More concisely: For any natural number `n`, the product of `n + 1` and the central binomial coefficient of `n + 1` equals twice the product of `2n + 1` and the central binomial coefficient of `n`. In Lean notation, `(n + 1) * binom (2*n + 1, n + 1) = 2 * (2*n + 1) * binom (2*n, n)`.
|
Nat.four_pow_le_two_mul_self_mul_centralBinom
theorem Nat.four_pow_le_two_mul_self_mul_centralBinom : ∀ (n : ℕ), 0 < n → 4 ^ n ≤ 2 * n * n.centralBinom
This theorem, named `Nat.four_pow_le_two_mul_self_mul_centralBinom`, states an exponential lower bound on the central binomial coefficient for all positive natural numbers. Specifically, the theorem states that for all positive natural numbers `n`, the value of `4^n` is less than or equal to the value of `2*n` times the central binomial coefficient of `n`. Despite being weaker than the theorem `Nat.four_pow_lt_mul_centralBinom`, this theorem holds historical significance as it was used in Erdős's proof of Bertrand's postulate.
More concisely: For all positive natural numbers `n`, $4^n \leq 2\times n \times \binom{2n}{n}$.
|
Nat.four_pow_lt_mul_centralBinom
theorem Nat.four_pow_lt_mul_centralBinom : ∀ (n : ℕ), 4 ≤ n → 4 ^ n < n * n.centralBinom
This theorem states that for any natural number `n` greater than or equal to 4, the value of 4 raised to the power `n` is less than `n` multiplied by the "central binomial coefficient" of `n`. The central binomial coefficient of `n` is a particular binomial coefficient that occurs in the middle of the `n`th row of Pascal's Triangle. This theorem is significant because it is used in Tochiori's refinement of Erdős's proof of Bertrand's postulate.
More concisely: For any natural number `n` greater than or equal to 4, $4^n < n \choose \frac{n}{2}$.
|