Nat.sum_range_choose
theorem Nat.sum_range_choose : ∀ (n : ℕ), ((Finset.range (n + 1)).sum fun m => n.choose m) = 2 ^ n
This theorem states that for any given natural number `n`, the sum of the binomial coefficients (`n.choose m`) for all `m` in the set of natural numbers less than `n + 1` (which is represented as `Finset.range (n + 1)`) is equal to `2^n`. In simpler terms, this theorem is saying that the sum of the entries in a particular row of Pascal's triangle is equal to 2 raised to the power of the row number, counting from zero (which is a well-known property of Pascal's triangle).
More concisely: The sum of binomial coefficients `n.choose m` for all `m` in the range `0` to `n`, is equal to `2^n`.
|
add_pow
theorem add_pow :
∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (n : ℕ),
(x + y) ^ n = (Finset.range (n + 1)).sum fun m => x ^ m * y ^ (n - m) * ↑(n.choose m)
The **binomial theorem** states that for any commutative semiring `R` and any elements `x` and `y` of `R`, the `n`-th power of the sum of `x` and `y` is equal to the sum, as `m` ranges from `0` to `n`, of the product of `x` to the power `m`, `y` to the power `(n - m)`, and the binomial coefficient `n choose m`. This binomial coefficient represents the number of ways to choose `m` elements from a set of `n` elements. The theorem can be represented mathematically as: \((x + y)^n = \sum_{m=0}^{n} x^m y^{n-m} \binom{n}{m}\).
More concisely: For any commutative semiring `R` and elements `x` and `y` in `R`, the `n`-th power of `x + y` equals the sum, over `m` from 0 to `n`, of `x^m * y^(n-m)` multiplied by the binomial coefficient `n choose m`.
|
Finset.sum_choose_succ_mul
theorem Finset.sum_choose_succ_mul :
∀ {R : Type u_3} [inst : NonAssocSemiring R] (f : ℕ → ℕ → R) (n : ℕ),
((Finset.range (n + 2)).sum fun i => ↑((n + 1).choose i) * f i (n + 1 - i)) =
((Finset.range (n + 1)).sum fun i => ↑(n.choose i) * f i (n + 1 - i)) +
(Finset.range (n + 1)).sum fun i => ↑(n.choose i) * f (i + 1) (n - i)
This theorem states that for any type `R` that is a non-associative semiring and any function `f` from two natural numbers to `R`, the sum of the product of the binomial coefficient "n+1 choose i" and `f(i, n+1-i)` over all natural numbers less than `n+2` is equal to the sum of two separate sums over all natural numbers less than `n+1`. The first sum is the product of the binomial coefficient "n choose i" and `f(i, n+1-i)`, and the second sum is the product of the binomial coefficient "n choose i" and `f(i+1, n-i)`. This means that you can split a sum that goes up to `n+2` into two sums that go up to `n+1` with slightly modified terms.
More concisely: For any non-associative semiring type R and function f from ℕ² to R, ∑\_{i=0}^{n+1} (i Chooses n-i) * f(i, n-i) + ∑\_{i=0}^{n} (i Chooses n-i) * f(i+1, n-i) = ∑\_{i=0}^{n+1} (n Chooses i) * f(i, n+1-i).
|
Nat.sum_Icc_choose
theorem Nat.sum_Icc_choose : ∀ (n k : ℕ), ((Finset.Icc k n).sum fun m => m.choose k) = (n + 1).choose (k + 1) := by
sorry
This theorem is known as "Zhu Shijie's identity" or the "hockey-stick identity". For every pair of natural numbers `n` and `k`, it states that the sum of the binomial coefficients `m choose k` for every `m` in the finite set of natural numbers from `k` to `n` (inclusive) is equal to the binomial coefficient `(n + 1) choose (k + 1)`. In mathematical terms, it is written as $\sum_{m=k}^{n} {m \choose k} = {n+1 \choose k+1}$.
More concisely: The sum of the binomial coefficients of `k` choose `m` for all `m` from `k` to `n` equals the binomial coefficient of `(n+1)` choose `(k+1)`. In other words, $\sum\_{m=k}^n {m \choose k} = {n+1 \choose k+1}$.
|
Finset.sum_antidiagonal_choose_succ_mul
theorem Finset.sum_antidiagonal_choose_succ_mul :
∀ {R : Type u_3} [inst : NonAssocSemiring R] (f : ℕ → ℕ → R) (n : ℕ),
((Finset.antidiagonal (n + 1)).sum fun ij => ↑((n + 1).choose ij.1) * f ij.1 ij.2) =
((Finset.antidiagonal n).sum fun ij => ↑(n.choose ij.1) * f ij.1 (ij.2 + 1)) +
(Finset.antidiagonal n).sum fun ij => ↑(n.choose ij.2) * f (ij.1 + 1) ij.2
This theorem states that for any non-associative semiring `R`, for any function `f` mapping two natural numbers to `R`, and for any natural number `n`, the sum of the product of "n+1 choose i" and `f(i, j)` over all (i, j) in the antidiagonal of `n+1`, is equal to the sum of the product of "n choose i" and `f(i, j+1)` over all (i, j) in the antidiagonal of `n` plus the sum of the product of "n choose j" and `f(i+1, j)` over all (i, j) in the antidiagonal of `n`. Here, the antidiagonal of a natural number `n` is the set of pairs of natural numbers (i, j) such that i + j = n.
More concisely: For any non-associative semiring `R` and function `f` mapping two natural numbers to `R`, the sum of the products of "n+1 choose i" and `f(i, j)` over the antidiagonal of `n+1` equals the sum of the products of "n choose i" and `f(i, j+1)` over the antidiagonal of `n` plus the sum of the products of "n choose j" and `f(i+1, j)` over the antidiagonal of `n`, where the antidiagonal of `n` is the set of pairs (i, j) such that i + j = n.
|
Commute.add_pow'
theorem Commute.add_pow' :
∀ {R : Type u_1} [inst : Semiring R] {x y : R},
Commute x y → ∀ (n : ℕ), (x + y) ^ n = (Finset.antidiagonal n).sum fun m => n.choose m.1 • (x ^ m.1 * y ^ m.2)
This theorem states that for any semiring `R` and any two elements `x` and `y` of `R` that commute (i.e. `x * y = y * x`), for any natural number `n`, the `n`-th power of the sum of `x` and `y` is equal to the sum, over all pairs `(i, j)` in the `n`-th antidiagonal, of the `n` choose `i` scalar multiple of the product of `x` raised to the power `i` and `y` raised to the power `j`. Here, the `n`-th antidiagonal is the set of all pairs `(i, j)` of natural numbers such that `i + j = n`.
More concisely: For any commuting elements `x` and `y` in a semiring `R` and natural number `n`, the sum of their `n`-th powers equals the sum, over the `n`-th antidiagonal, of the scalar multiples of the product of `x` raised to the `i`-th power and `y` raised to the `j`-th power, where `i + j = n`.
|
Commute.add_pow
theorem Commute.add_pow :
∀ {R : Type u_1} [inst : Semiring R] {x y : R},
Commute x y → ∀ (n : ℕ), (x + y) ^ n = (Finset.range (n + 1)).sum fun m => x ^ m * y ^ (n - m) * ↑(n.choose m)
This theorem is a version of the **binomial theorem** for noncommutative semirings. It states that for any semiring `R`, and any two elements `x` and `y` in `R` that commute (meaning `x * y = y * x`), for any natural number `n`, the `n`-th power of the sum of `x` and `y` equals the sum, taken over all natural numbers less than or equal to `n`, of the product of the `m`-th power of `x`, the `(n - m)`-th power of `y`, and the binomial coefficient `n choose m`. In mathematical notation, this is expressed as `(x + y)^n = Σ_{m=0}^{n} (x^m * y^(n - m) * (n choose m))`.
More concisely: For any commuting elements `x` and `y` in a semiring `R` and natural number `n`, the `n`-th power of `x + y` equals the sum, over all `m` from `0` to `n`, of the product of `x^m * y^(n - m) * (n choose m)`.
|