Finset.Nat.prod_antidiagonal_eq_prod_range_succ
theorem Finset.Nat.prod_antidiagonal_eq_prod_range_succ :
∀ {M : Type u_3} [inst : CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ),
((Finset.antidiagonal n).prod fun ij => f ij.1 ij.2) = (Finset.range n.succ).prod fun k => f k (n - k)
This theorem states that for any commutative monoid `M` and any function `f` from pairs of natural numbers to `M`, the product over the antidiagonal of a natural number `n` (i.e., the set of pairs `(i, j)` such that `i + j = n`) under `f` is equal to the product over the range `n.succ` (i.e., the set of natural numbers less than `n + 1`) under `f` applied to `k` and `n - k`. In other words, the product of the function values on the antidiagonal is the same as the product of the function values on the range, when the function arguments are suitably adjusted.
More concisely: For any commutative monoid `M` and function `f` from pairs of natural numbers to `M`, the product of `f` over the antidiagonal of a natural number `n` equals the product of `f` applied to `k` and `n - k` over the range `n.succ`.
|
Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk
theorem Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk :
∀ {M : Type u_3} [inst : AddCommMonoid M] (f : ℕ × ℕ → M) (n : ℕ),
((Finset.antidiagonal n).sum fun ij => f ij) = (Finset.range n.succ).sum fun k => f (k, n - k)
The theorem `Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk` states that for any type `M` equipped with an additive commutative monoid structure and any function `f` from tuples of natural numbers to `M`, for any natural number `n`, the sum of `f` evaluated at each element of the antidiagonal of `n` is equal to the sum of `f` evaluated at each element `(k, n - k)` where `k` ranges over the set of natural numbers less than `n + 1`. In other words, the sum over the antidiagonal set is redistributed into a sum over the range set with adjusted indices in `f`. This theorem is a statement about the equivalence of two methods of summing over certain sets of natural numbers.
More concisely: For any additive commutative monoid-valued function `f` and natural number `n`, the sum of `f` over the antidiagonal of `n` equals the sum over the set `{(k, n - k) | k < n + 1}` in `f`.
|
Finset.Nat.sum_antidiagonal_eq_sum_range_succ
theorem Finset.Nat.sum_antidiagonal_eq_sum_range_succ :
∀ {M : Type u_3} [inst : AddCommMonoid M] (f : ℕ → ℕ → M) (n : ℕ),
((Finset.antidiagonal n).sum fun ij => f ij.1 ij.2) = (Finset.range n.succ).sum fun k => f k (n - k)
This theorem, `Finset.Nat.sum_antidiagonal_eq_sum_range_succ`, states that for any type `M` equipped with an additive commutative monoid structure, a function `f` from pairs of natural numbers to `M`, and a natural number `n`, the sum of `f` over the antidiagonal of `n` is equal to the sum of `f` over the range of `n + 1`, where the function `f` is applied to each element `k` in the range and `n - k`. In other words, summing up `f(i, j)` for all `(i, j)` in the antidiagonal of `n` (i.e., all pairs of nonnegative integers that add up to `n`) gives the same result as summing up `f(k, n - k)` for all `k` from `0` to `n`.
More concisely: For any additive commutative monoid-valued function `f` on pairs of natural numbers, the sum of `f` over the antidiagonal of size `n` equals the sum over the range from `0` to `n` applying `f` to `(k, n - k)`.
|