MvPolynomial.esymm_eq_sum_monomial
theorem MvPolynomial.esymm_eq_sum_monomial :
∀ (σ : Type u_1) (R : Type u_2) [inst : CommSemiring R] [inst_1 : Fintype σ] (n : ℕ),
MvPolynomial.esymm σ R n =
(Finset.powersetCard n Finset.univ).sum fun t => (MvPolynomial.monomial (t.sum fun i => fun₀ | i => 1)) 1
The theorem `MvPolynomial.esymm_eq_sum_monomial` states that for any types `σ` and `R`, where `R` is a commutative semiring and `σ` is a fintype, and for any natural number `n`, the `n`-th elementary symmetric multivariate polynomial `MvPolynomial.esymm σ R n` can be expressed as a sum over explicit monomials. More specifically, it can be written as the sum, over all subsets of cardinality `n` of a universal set of `σ`, of the monomials where each element in the subset contributes an exponent of 1 and the coefficient is 1.
More concisely: For any commutative semiring `R` and finite type `σ`, the `n`-th elementary symmetric multivariate polynomial `MvPolynomial.esymm σ R n` equals the sum of monomials, each with a coefficient of 1 and exponents corresponding to any subset of cardinality `n` of `σ`.
|
MvPolynomial.esymm_eq_sum_subtype
theorem MvPolynomial.esymm_eq_sum_subtype :
∀ (σ : Type u_1) (R : Type u_2) [inst : CommSemiring R] [inst_1 : Fintype σ] (n : ℕ),
MvPolynomial.esymm σ R n = Finset.univ.sum fun t => (↑t).prod fun i => MvPolynomial.X i
The theorem `MvPolynomial.esymm_eq_sum_subtype` states that for any types σ and R, where R is a commutative semiring and σ is a finite type, and any natural number n, the n-th elementary symmetric multivariate polynomial over σ and R can be defined as the sum over all elements of the universal set (which is implied from the assumption that σ is finite), where each element is the product of the degree-1 monomial $X_i$ for each i in that element. This provides an alternative definition of the elementary symmetric polynomial which sums over a subtype instead of the power set of a certain length.
More concisely: For any commutative semiring R and finite type σ, the n-th elementary symmetric multivariate polynomial over σ and R is the sum, over all subsets S of σ with |S| = n, of the products of degree-1 monomials indexed by elements in S.
|
MvPolynomial.esymm_eq_multiset_esymm
theorem MvPolynomial.esymm_eq_multiset_esymm :
∀ (σ : Type u_1) (R : Type u_2) [inst : CommSemiring R] [inst_1 : Fintype σ],
MvPolynomial.esymm σ R = (Multiset.map MvPolynomial.X Finset.univ.val).esymm
The theorem `MvPolynomial.esymm_eq_multiset_esymm` states that for any given type `σ`, type `R`, and under the assumptions that `R` has a structure of `CommSemiring` and `σ` has a `Fintype` instance, the `n`th elementary symmetric multivariate polynomial over `σ` and `R`, denoted `MvPolynomial.esymm σ R`, is obtained by evaluating the `n`th elementary symmetric function at the multiset of degree `1` monomials. In other words, this theorem connects the notion of an elementary symmetric polynomial with the operation of mapping the function `MvPolynomial.X` (which generates a degree `1` monomial) over the universal finite set of type `σ`.
More concisely: The `n`th elementary symmetric polynomial over a `Fintype` σ and a `CommSemiring` R is equal to the multiset evaluation of the `n`th elementary function on the monomials generated by `MvPolynomial.X` over σ.
|
Finset.esymm_map_val
theorem Finset.esymm_map_val :
∀ {R : Type u_1} [inst : CommSemiring R] {σ : Type u_2} (f : σ → R) (s : Finset σ) (n : ℕ),
(Multiset.map f s.val).esymm n = (Finset.powersetCard n s).sum fun t => t.prod f
The theorem `Finset.esymm_map_val` states that for any type `R` equipped with a commutative semiring structure, a function `f` from type `σ` to `R`, a finite set `s` of elements of type `σ`, and a natural number `n`, the `n`th elementary symmetric function evaluated at the elements of the multiset obtained by mapping `f` over the elements of `s` is equal to the sum, over all subsets of `s` of cardinality `n`, of the product of the function `f` applied to the elements of each subset. In other words, it links elementary symmetric functions with a sum of products over subsets of a fixed cardinality.
More concisely: For any commutative semiring `R`, function `f` from type `σ` to `R`, finite set `s` of elements of type `σ`, and natural number `n`, the `n`th elementary symmetric function of the multiset obtained by mapping `f` over the elements of `s` equals the sum of products of `f` applied to subsets of `s` of size `n`.
|