bernoulli'_zero
theorem bernoulli'_zero : bernoulli' 0 = 1
The theorem `bernoulli'_zero` states that the zeroth Bernoulli number, which is denoted as $B_0$ in mathematical notation, is equal to 1. In line with the recursive definition of the Bernoulli numbers, this theorem provides the base case where n equals zero.
More concisely: The zeroth Bernoulli number $B\_0$ equals 1.
|
sum_range_pow
theorem sum_range_pow :
∀ (n p : ℕ),
((Finset.range n).sum fun k => ↑k ^ p) =
(Finset.range (p + 1)).sum fun i => bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
This is **Faulhaber's theorem**, which provides a relationship between the sum of p-th powers of natural numbers and the Bernoulli numbers. More specifically, it states that the sum of the p-th powers of the natural numbers less than n is equal to the sum, over all i from 0 to p, of the i-th Bernoulli number times the binomial coefficient of p+1 choose i, all multiplied by n raised to the power of p+1-i, and divided by p+1.
More concisely: The sum of the n-th powers of the first i natural numbers equals the ratio of the i-th Bernoulli number to (p+1) times the sum of the binomial coefficients of (p+1) choose i, all multiplied by n raised to the power of p+1-i.
|
bernoulli'_one
theorem bernoulli'_one : bernoulli' 1 = 1 / 2
The theorem `bernoulli'_one` states that the first Bernoulli number, denoted by `bernoulli' 1`, is equal to one-half. In other words, when we calculate the Bernoulli number for the case where `n` is `1` using the defined recursive function, the result is `1/2`.
More concisely: The first Bernoulli number equals 1/2.
|
bernoulli'_odd_eq_zero
theorem bernoulli'_odd_eq_zero : ∀ {n : ℕ}, Odd n → 1 < n → bernoulli' n = 0
This theorem states that for any natural number `n`, if `n` is an odd number and `n` is greater than 1, then the `n`th Bernoulli number equals zero. In other words, all odd Bernoulli numbers, with the exception of the first one, are zero.
More concisely: For any odd natural number `n` greater than 1, the `n`th Bernoulli number is zero.
|
bernoulli'_def
theorem bernoulli'_def :
∀ (n : ℕ), bernoulli' n = 1 - (Finset.range n).sum fun k => ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k
The theorem `bernoulli'_def` states that for all natural numbers `n`, the `n`-th Bernoulli number `B_n`, as represented by the function `bernoulli' n`, is equal to `1` minus the sum over all natural numbers `k` less than `n` (represented by `Finset.range n`) of the binomial coefficient `n choose k` (represented by `Nat.choose n k`) divided by `(n - k + 1)` times the `k`-th Bernoulli number `B_k`. This sum is represented in Lean by `Finset.sum (Finset.range n) fun k => ↑(Nat.choose n k) / (↑n - ↑k + 1) * bernoulli' k`, and corresponds to the mathematical formula `1 - \sum_{k < n} \binom{n}{k}\frac{B_k}{n+1-k}`.
More concisely: The `n`-th Bernoulli number `B_n` is equal to `1` minus the sum over all `0 < k < n` of the binomial coefficient `n choose k` divided by `(n - k + 1)` times the `k`-th Bernoulli number `B_k`.
|
bernoulli_eq_bernoulli'_of_ne_one
theorem bernoulli_eq_bernoulli'_of_ne_one : ∀ {n : ℕ}, n ≠ 1 → bernoulli n = bernoulli' n
This theorem states that for any natural number 'n', if 'n' is not equal to 1, then the value of the Bernoulli number (as defined by the `bernoulli` function) for 'n' is equal to the value of the Bernoulli number according to the alternative definition provided by the `bernoulli'` function. The Bernoulli numbers are a sequence of rational numbers which are important in number theory and analysis.
More concisely: For all natural numbers n exceeding 1, the Bernoulli number `bernoulli n` equals the Bernoulli number according to the alternative definition `bernoulli' n`.
|
sum_Ico_pow
theorem sum_Ico_pow :
∀ (n p : ℕ),
((Finset.Ico 1 (n + 1)).sum fun k => ↑k ^ p) =
(Finset.range (p + 1)).sum fun i => bernoulli' i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
This statement presents an alternate form of Faulhaber's theorem, which establishes a relationship between the sum of p-th powers of natural numbers and the Bernoulli numbers. Specifically, it states that for any natural numbers `n` and `p`, the sum of the `p`-th powers of all natural numbers from `1` to `n` is equal to the sum of the product of the `i`-th Bernoulli number, the binomial coefficient of `p+1` choose `i`, and `n` to the power of `p+1-i`, all divided by `p+1`, for all `i` in the range from `0` to `p`. This is represented in mathematical notation as:
$$\sum_{k=1}^{n} k^p = \sum_{i=0}^p (-1)^iB_i\binom{p+1}{i}\frac{n^{p+1-i}}{p+1}.$$
The theorem is derived from the `sum_range_pow` theorem.
More concisely: The sum of the `p`-th powers of the first `n` natural numbers equals the sum of the products of the corresponding Bernoulli numbers, binomial coefficients, and `n` raised to the power of the difference between `p+1` and the index, all divided by `p+1`.
|