MvPolynomial.weightedTotalDegree'_zero
theorem MvPolynomial.weightedTotalDegree'_zero :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
[inst_2 : SemilatticeSup M] (w : σ → M), MvPolynomial.weightedTotalDegree' w 0 = ⊥
The theorem `MvPolynomial.weightedTotalDegree'_zero` states that for any commutative semiring `R`, any type `σ`, any additively commutative monoid `M` with a semilattice sup structure, and any function `w: σ → M`, the weighted total degree of the zero polynomial (a multivariate polynomial where all coefficients are zero) is `⊥` (the bottom element in the semilattice). This means that the zero polynomial, regardless of the weights assigned to its variables, has the lowest possible total degree.
More concisely: For any commutative semiring R, additively commutative monoid M with a semilattice sup structure, and function w : σ -> M, the weighted total degree of the zero multivariate polynomial over (R, M, w) is ⊥.
|
MvPolynomial.IsWeightedHomogeneous.coeff_eq_zero
theorem MvPolynomial.IsWeightedHomogeneous.coeff_eq_zero :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
{φ : MvPolynomial σ R} {n : M} {w : σ → M},
MvPolynomial.IsWeightedHomogeneous w φ n →
∀ (d : σ →₀ ℕ), (MvPolynomial.weightedDegree w) d ≠ n → MvPolynomial.coeff d φ = 0
This theorem states that, given a commutative semiring `R`, an additive commutative monoid `M`, and a multivariate polynomial `φ` over `σ` variables with coefficients in `R`, if `φ` is a weighted homogeneous polynomial of weighted degree `n` with weight function `w`, then for any monomial `d`, if the weighted degree of `d` according to `w` is not equal to `n`, then the coefficient of `d` in the polynomial `φ` is zero. In other words, the support of a weighted homogeneous polynomial is controlled by its weighted degree: any monomial that doesn't have this degree doesn't appear in the polynomial.
More concisely: A weighted homogeneous polynomial of weighted degree `n` with weight function `w` over a commutative semiring `R` and an additive commutative monoid `M` has coefficient zero for any monomial of weighted degree different from `n`.
|
MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported
theorem MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported :
∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
(m : M),
MvPolynomial.weightedHomogeneousSubmodule R w m =
Finsupp.supported R R {d | (MvPolynomial.weightedDegree w) d = m}
The theorem `MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported` asserts that given a commutative semiring `R`, an additively commutative monoid `M`, and a function `w` from `σ` to `M`, for any value `m` in `M`, the submodule of homogeneous multivariate polynomials (denoted `MvPolynomial.weightedHomogeneousSubmodule R w m`) of a certain degree `m` is the same as the `R`-submodule (denoted `Finsupp.supported R R {d | (MvPolynomial.weightedDegree w) d = m}`) of all finitely supported functions `p` from `(σ →₀ ℕ)` to `R` such that the support of `p` is a subset of the set of degrees `d` where the weighted degree of `d` with respect to `w` equals `m`. Despite being equal, the former submodule has a more convenient definitional reduction.
More concisely: The submodule of weighted homogeneous multivariate polynomials of degree `m` with respect to a weight function `w` is equal to the submodule generated by finitely supported functions whose degrees have weighted degree `m` with respect to `w`.
|
MvPolynomial.isWeightedHomogeneous_C
theorem MvPolynomial.isWeightedHomogeneous_C :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
(r : R), MvPolynomial.IsWeightedHomogeneous w (MvPolynomial.C r) 0
This theorem states that for any commutative semiring `R`, any type `σ`, and any additive commutative monoid `M`, any weighted function `w : σ → M`, and any element `r` of `R`, the constant polynomial `C r` is weighted homogeneous of degree 0. In other words, in the multivariate polynomial generated by `r`, all monomials have a weighted degree of 0.
More concisely: For any commutative semiring `R`, any type `σ`, additive commutative monoid `M`, weighted function `w : σ → M`, and element `r` of `R`, the constant polynomial `C r` is weighted homogeneous of degree 0 with respect to `w`.
|
MvPolynomial.sum_weightedHomogeneousComponent
theorem MvPolynomial.sum_weightedHomogeneousComponent :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
(φ : MvPolynomial σ R), (finsum fun m => (MvPolynomial.weightedHomogeneousComponent w m) φ) = φ
This theorem states that any multivariate polynomial, denoted here as `φ`, can be expressed as the sum of its weighted homogeneous components. Here, `R` is the coefficient ring, `σ` is the index set of the variables, and `M` is an additive commutative monoid. The function `w` assigns a weight to each variable in `σ`, and `MvPolynomial.weightedHomogeneousComponent w m` is the weighted homogeneous component of `φ` of degree `m`. The function `finsum` is a sum over all these components. Therefore, this theorem asserts that for every multivariate polynomial `φ`, the sum over all its weighted homogeneous components equals `φ` itself.
More concisely: Every multivariate polynomial can be expressed as the sum of its weighted homogeneous components with respect to given weights.
|
MvPolynomial.isWeightedHomogeneous_zero
theorem MvPolynomial.isWeightedHomogeneous_zero :
∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
(m : M), MvPolynomial.IsWeightedHomogeneous w 0 m
The theorem `MvPolynomial.isWeightedHomogeneous_zero` states that, for any commutative semiring `R`, any type `M` with a given additive commutative monoid structure, any type `σ`, any function `w` from `σ` to `M`, and any element `m` of `M`, the multivariate polynomial `0` is weighted homogeneous of degree `m`. In other words, all the monomials occurring in the `0` polynomial have a weighted degree of `m`, which is a property defined by the function `w`.
More concisely: For any commutative semiring R, additive commutative monoid M with unit, type σ, function w from σ to M, and element m of M, the multivariate polynomial 0 is weighted homogeneous of degree m with respect to w.
|
MvPolynomial.IsWeightedHomogeneous.sum
theorem MvPolynomial.IsWeightedHomogeneous.sum :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {ι : Type u_4}
(s : Finset ι) (φ : ι → MvPolynomial σ R) (n : M) {w : σ → M},
(∀ i ∈ s, MvPolynomial.IsWeightedHomogeneous w (φ i) n) →
MvPolynomial.IsWeightedHomogeneous w (s.sum fun i => φ i) n
The theorem states that the sum of weighted homogeneous multivariate polynomials of degree `n` is also a weighted homogeneous multivariate polynomial of degree `n`. Here, `R` is the coefficient ring of the polynomials, `σ` is the index set of the variables, `M` is an additive commutative monoid that represents the weight space, and `ι` is the index set of the polynomials in the sum. The function `φ` maps indices to polynomials, the function `w` assigns weights to the variables, and `s` is a finite set of indices. The condition of the theorem is that for each index `i` in `s`, the polynomial `φ i` is weighted homogeneous of degree `n` with respect to the weight function `w`. The conclusion is that the sum of the polynomials `φ i` for `i` in `s` is also weighted homogeneous of degree `n` with respect to `w`.
More concisely: Given a ring R, an additive commutative monoid M as weight space, an index set σ, a function φ mapping indices to weighted homogeneous multivariate polynomials of degree n, and a finite set s of indices such that for all i in s, φ(i) is weighted homogeneous of degree n with respect to weight function w, then the sum of φ(i) for i in s is also weighted homogeneous of degree n with respect to w.
|
MvPolynomial.IsWeightedHomogeneous.inj_right
theorem MvPolynomial.IsWeightedHomogeneous.inj_right :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
{φ : MvPolynomial σ R} {m n : M} {w : σ → M},
φ ≠ 0 → MvPolynomial.IsWeightedHomogeneous w φ m → MvPolynomial.IsWeightedHomogeneous w φ n → m = n
The theorem `MvPolynomial.IsWeightedHomogeneous.inj_right` states that for any non-zero multivariate polynomial, if it is weighted homogeneous of weighted degree `m` and also of weighted degree `n` (which essentially means all monomials in the polynomial have the same weighted degree), then `m` must equal `n`. This means the weighted degree of a non-zero weighted homogeneous polynomial is well-defined and unique. This is formulated over an arbitrary commutative semiring `R` and an arbitrary add commutative monoid `M`, with `σ` representing the index set of the variables in the polynomial and `w` representing the weight function.
More concisely: For any non-zero multivariate polynomial over an arbitrary commutative semiring and an add commutative monoid with a weight function, if it is weighted homogeneous with two equal weighted degrees, then the weighted degrees are equal and uniquely determine the weighted homogeneous polynomial.
|
MvPolynomial.weightedTotalDegree'_eq_bot_iff
theorem MvPolynomial.weightedTotalDegree'_eq_bot_iff :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
[inst_2 : SemilatticeSup M] (w : σ → M) (p : MvPolynomial σ R),
MvPolynomial.weightedTotalDegree' w p = ⊥ ↔ p = 0
This theorem states that for any commutative semiring `R`, any AddCommMonoid `M`, any type `σ`, any weight function `w : σ → M`, and any multivariate polynomial `p` over the variables indexed by `σ` with coefficients from `R`, the `weightedTotalDegree'` of the polynomial `p` is `⊥` (which in this context represents the least element in the semilattice `M`, often interpreted as "undefined" or "minus infinity") if and only if `p` is the zero polynomial. In other words, a multivariate polynomial has undefined or minus infinity weighted total degree if and only if it is the zero polynomial.
More concisely: For any commutative semiring R, AddCommMonoid M, type σ, weight function w : σ → M, and multivariate polynomial p over σ with coefficients from R, the weighted total degree of p is minimal (or least) element in M if and only if p is the zero polynomial.
|
MvPolynomial.IsWeightedHomogeneous.mul
theorem MvPolynomial.IsWeightedHomogeneous.mul :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
{φ ψ : MvPolynomial σ R} {m n : M} {w : σ → M},
MvPolynomial.IsWeightedHomogeneous w φ m →
MvPolynomial.IsWeightedHomogeneous w ψ n → MvPolynomial.IsWeightedHomogeneous w (φ * ψ) (m + n)
The theorem `MvPolynomial.IsWeightedHomogeneous.mul` states that given a commutative semiring `R`, an additive commutative monoid `M`, and `σ` indexing the variables in a multivariate polynomial, if `φ` and `ψ` are multivariate polynomials that are weighted homogeneous of weighted degrees `m` and `n` respectively, then the product of `φ` and `ψ` is a multivariate polynomial that is weighted homogeneous of weighted degree `m + n`. In other words, if each term in `φ` and `ψ` has a consistent weighted degree according to some weight function `w`, their product will have a weighted degree that is the sum of their individual weighted degrees.
More concisely: Given multivariate polynomials `φ` and `ψ` over a commutative semiring `R` with additive commutative monoid `M`, if `φ` is weighted homogeneous of degree `m` and `ψ` is weighted homogeneous of degree `n` with respect to some weight function `w`, then their product `φ ψ` is weighted homogeneous of degree `m + n`.
|
MvPolynomial.isWeightedHomogeneous_X
theorem MvPolynomial.isWeightedHomogeneous_X :
∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
(i : σ), MvPolynomial.IsWeightedHomogeneous w (MvPolynomial.X i) (w i)
This theorem states that for any commutative semiring `R`, additive commutative monoid `M`, and a function `w` from `σ` (which could represent variables in a multivariate polynomial) to `M` (representing the weights), an indeterminate `i` (which is a specific variable in `σ`) is considered to be weighted homogeneous of degree `w i` under the weighting function `w`. In simpler terms, in the context of weighted homogeneous multivariate polynomials, a single variable term (or an indeterminate) has a weighted degree equal to its weight as assigned by the function `w`.
More concisely: For any commutative semiring `R`, additive commutative monoid `M`, and weight function `w` from variables to `M`, an indeterminate's weighted degree equals its weight under `w` in the context of weighted homogeneous multivariate polynomials over `R` and `M`.
|
MvPolynomial.isWeightedHomogeneous_monomial
theorem MvPolynomial.isWeightedHomogeneous_monomial :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
(d : σ →₀ ℕ) (r : R) {m : M},
(MvPolynomial.weightedDegree w) d = m → MvPolynomial.IsWeightedHomogeneous w ((MvPolynomial.monomial d) r) m
The theorem `MvPolynomial.isWeightedHomogeneous_monomial` states that, for any commutative semiring `R`, additive commutative monoid `M`, function `w` from `σ` to `M`, finitely supported function `d` from `σ` to natural numbers `ℕ`, ring element `r` from `R`, and `m` from `M`, if the weighted degree of `d` under `w` equals `m`, then the multivariate polynomial that is the monomial of `d` with coefficient `r` is weighted homogeneous of weighted degree `m` under `w`. In other words, all monomials are weighted homogeneous.
More concisely: For any commutative semiring `R`, additive commutative monoid `M`, function `w` from a set `σ` to `M`, finitely supported function `d` from `σ` to natural numbers `ℕ`, ring element `r` from `R`, and `m` from `M`, if the weighted degree of `d` under `w` equals `m`, then the multivariate polynomial with coefficient `r` formed from the monomial `m` is weighted homogeneous of degree `m` under `w`.
|
MvPolynomial.weightedHomogeneousSubmodule_mul
theorem MvPolynomial.weightedHomogeneousSubmodule_mul :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
(m n : M),
MvPolynomial.weightedHomogeneousSubmodule R w m * MvPolynomial.weightedHomogeneousSubmodule R w n ≤
MvPolynomial.weightedHomogeneousSubmodule R w (m + n)
The theorem `MvPolynomial.weightedHomogeneousSubmodule_mul` states that for any commutative semiring `R`, any additive commutative monoid `M`, any function `w` from `σ` to `M`, and any elements `m` and `n` of `M`, the submodule generated by the product of weighted homogeneous polynomials of degrees `m` and `n` (respectively `MvPolynomial.weightedHomogeneousSubmodule R w m` and `MvPolynomial.weightedHomogeneousSubmodule R w n`) is contained within the submodule of weighted homogeneous polynomials of degree `m + n` (`MvPolynomial.weightedHomogeneousSubmodule R w (m + n)`). In simpler terms, when you multiply two weighted homogeneous polynomials of degrees `m` and `n`, the result is a polynomial that can be classified as a weighted homogeneous polynomial of degree `m + n`.
More concisely: For any commutative semiring R, additive commutative monoid M, and function w from σ to M, the submodule generated by the products of weighted homogeneous polynomials of degrees m and n in MvPolynomial.weightedHomogeneousSubmodule R w (m) and MvPolynomial.weightedHomogeneousSubmodule R w (n) is contained in MvPolynomial.weightedHomogeneousSubmodule R w (m + n).
|
MvPolynomial.isWeightedHomogeneous_one
theorem MvPolynomial.isWeightedHomogeneous_one :
∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M),
MvPolynomial.IsWeightedHomogeneous w 1 0
The theorem `MvPolynomial.isWeightedHomogeneous_one` states that for any type `R` with a commutative semiring structure, any type `M` with an additive commutative monoid structure, and any function `w` from type `σ` to `M`, the multivariate polynomial `1` is weighted homogeneous of weighted degree `0`. In other words, all the monomials occurring in the multivariate polynomial `1` have a weighted degree of `0`, regardless of the weight function `w`.
More concisely: For any commutative semiring `R`, additive commutative monoid `M`, and weight function `w` from type `σ` to `M`, the constant polynomial `1` in `R[X1, ..., Xn]` is weighted homogeneous of degree `0` with respect to `w`.
|
MvPolynomial.weightedHomogeneousComponent_isWeightedHomogeneous
theorem MvPolynomial.weightedHomogeneousComponent_isWeightedHomogeneous :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M}
(n : M) (φ : MvPolynomial σ R),
MvPolynomial.IsWeightedHomogeneous w ((MvPolynomial.weightedHomogeneousComponent w n) φ) n
This theorem states that for any commutative semiring `R`, any additive commutative monoid `M`, any indexing set `σ`, any weight function `w` from `σ` to `M`, any element `n` of `M`, and any multivariate polynomial `φ` with coefficients in `R` and variables indexed by `σ`, the `n`-th weighted homogeneous component of `φ` is a weighted homogeneous polynomial of weighted degree `n`. In other words, all monomials in this component of the polynomial have a weighted degree equal to `n` according to the weight function `w`.
More concisely: For any commutative semiring `R`, additive commutative monoid `M`, indexing set `σ`, weight function `w` from `σ` to `M`, element `n` of `M`, and multivariate polynomial `φ` with coefficients in `R` and variables indexed by `σ`, the `n`-th weighted homogeneous component of `φ` is a weighted homogeneous polynomial with weighted degree `n` with respect to `w`.
|
MvPolynomial.IsWeightedHomogeneous.prod
theorem MvPolynomial.IsWeightedHomogeneous.prod :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {ι : Type u_4}
(s : Finset ι) (φ : ι → MvPolynomial σ R) (n : ι → M) {w : σ → M},
(∀ i ∈ s, MvPolynomial.IsWeightedHomogeneous w (φ i) (n i)) →
MvPolynomial.IsWeightedHomogeneous w (s.prod fun i => φ i) (s.sum fun i => n i)
The theorem `MvPolynomial.IsWeightedHomogeneous.prod` states that given a finite set of indices `s` and a collection of multivariate polynomials `φ` indexed by `s` over a commutative semiring `R` and an index set `σ`, if each polynomial in the collection is weighted homogeneous with a weighted degree `n`, then the product of all these polynomials is also weighted homogeneous. Moreover, the weighted degree of this product is the sum of the weighted degrees of the individual polynomials. The "weight" of each variable in the polynomials is given by the function `w : σ → M`, where `M` is an additive commutative monoid.
More concisely: Given a finite set of multivariate polynomials over a commutative semiring, each weighted homogeneous with degree `n` and weights given by a function `w : σ → M`, the product of these polynomials is weighted homogeneous with degree `∑(n : ℕ) * w i` for all `i ∈ s`.
|
MvPolynomial.isWeightedHomogeneous_of_total_degree_zero
theorem MvPolynomial.isWeightedHomogeneous_of_total_degree_zero :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
[inst_2 : SemilatticeSup M] [inst_3 : OrderBot M] (w : σ → M) {p : MvPolynomial σ R},
MvPolynomial.weightedTotalDegree w p = ⊥ → MvPolynomial.IsWeightedHomogeneous w p ⊥
The theorem `MvPolynomial.isWeightedHomogeneous_of_total_degree_zero` states that for any commutative semiring `R`, any type `σ`, any additive commutative monoid `M` which is also a semilattice with a bottom element, and any weight function `w` from `σ` to `M`, if a multivariate polynomial `p` over `σ` and `R` has a weighted total degree of the bottom element under `w`, then `p` is a weighted homogeneous polynomial of degree `⊥` under `w`. In simpler terms, if a multivariate polynomial's weighted total degree is the lowest possible value, all of its monomials must also have this lowest possible weighted degree.
More concisely: If a multivariate polynomial over a commutative semiring has minimal weighted total degree under a given weight function, then it is weighted homogeneous of degree the bottom element with respect to that weight function.
|
MvPolynomial.weightedHomogeneousComponent_zero
theorem MvPolynomial.weightedHomogeneousComponent_zero :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : CanonicallyOrderedAddCommMonoid M]
{w : σ → M} (φ : MvPolynomial σ R) [inst_2 : NoZeroSMulDivisors ℕ M],
(∀ (i : σ), w i ≠ 0) →
(MvPolynomial.weightedHomogeneousComponent w 0) φ = MvPolynomial.C (MvPolynomial.coeff 0 φ)
This theorem states that if `M` is a `CanonicallyOrderedAddCommMonoid`, then the weighted homogeneous component of weighted degree `0` of a polynomial is its constant coefficient. In other words, for any multivariate polynomial `φ` defined over a commutative semiring `R` with variables indexed by `σ` and weights assigned to each variable (denoted by the function `w` from `σ` to `M`), if all weights are non-zero and there are no zero divisors with respect to multiplication in `M` and `ℕ`, the homogeneous component of `φ` of degree `0` (with respect to the weighting `w`) is precisely the constant coefficient of `φ` in `R`. The constant coefficient of `φ` is represented as `MvPolynomial.C (MvPolynomial.coeff 0 φ)`.
More concisely: For a multivariate polynomial `φ` over a commutative semiring `R` with non-zero, weighted variables `σ` and a CanonicallyOrderedAddCommMonoid `M` with no zero divisors in `M` and `ℕ`, the weighted homogeneous component of degree 0 of `φ` equals its constant coefficient in `M`.
|
MvPolynomial.weightedTotalDegree_zero
theorem MvPolynomial.weightedTotalDegree_zero :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
[inst_2 : SemilatticeSup M] [inst_3 : OrderBot M] (w : σ → M), MvPolynomial.weightedTotalDegree w 0 = ⊥
The theorem `MvPolynomial.weightedTotalDegree_zero` states that for any commutative semiring `R`, any additively commutative monoid `M` that also forms a semilattice under supremum operation and has a bottom element `⊥`, and any function `w` from a type `σ` to `M`, the weighted total degree of the zero polynomial in the multivariate polynomial ring over `σ` and `R` is the bottom element `⊥` in `M`.
More concisely: For any commutative semiring R, additively commutative monoid M with a bottom element ⊥, and function w from a type σ to M, the weighted total degree of the zero polynomial in the multivariate polynomial ring over σ and R is ⊥.
|
MvPolynomial.weightedHomogeneousComponent_weighted_homogeneous_polynomial
theorem MvPolynomial.weightedHomogeneousComponent_weighted_homogeneous_polynomial :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M}
[inst_2 : DecidableEq M] (m n : M),
∀ p ∈ MvPolynomial.weightedHomogeneousSubmodule R w n,
(MvPolynomial.weightedHomogeneousComponent w m) p = if m = n then p else 0
This theorem deals with multivariate polynomials that have a property called being "weighted homogeneous." Intuitively, a polynomial being "weighted homogeneous" means that all of its monomial terms have the same "weight." The notion of "weight" here is dependent on a weight function, which is a map from the set of variables to some additive monoid.
The theorem states that for any commutative semiring `R`, additive commutoid `M`, set of variables `σ`, weight function `w : σ → M`, and elements `m` and `n` in `M`, if a multivariate polynomial `p` is in the submodule of weighted homogeneous polynomials of weight `n`, then the weighted homogeneous component of `p` of weight `m` is `p` itself if `m` is equal to `n`, and is zero otherwise.
This theorem essentially gives a way to extract the "component" of a weighted homogeneous polynomial that corresponds to a certain weight. If the weight of the component we are trying to extract does not match the weight of the polynomial, then the component is simply zero.
More concisely: For any weight function and commutative semiring, a weighted homogeneous polynomial lies in the subspace spanned by its weighted homogeneous components of equal weight, and these components are zero for weights different than the polynomial's weight.
|
MvPolynomial.IsWeightedHomogeneous.weighted_total_degree
theorem MvPolynomial.IsWeightedHomogeneous.weighted_total_degree :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
{φ : MvPolynomial σ R} {n : M} [inst_2 : SemilatticeSup M] {w : σ → M},
MvPolynomial.IsWeightedHomogeneous w φ n → φ ≠ 0 → MvPolynomial.weightedTotalDegree' w φ = ↑n
This theorem states that for a non-zero multivariate polynomial `φ` with given weighted degree `n` and weight function `w`, if `φ` is weighted homogeneous of weighted degree `n`, then the weighted total degree of `φ` is `n`. This is true for any commutative semiring `R`, any index set of variables `σ`, and any type `M` which forms an additive commutative monoid and has a semilattice structure.
More concisely: For a non-zero multivariate polynomial `φ` over a commutative semiring `R`, if `φ` is weighted homogeneous of weighted degree `n` with respect to a weight function `w` and index set of variables `σ`, then the weighted total degree of `φ` is equal to `n`.
|
MvPolynomial.IsWeightedHomogeneous.add
theorem MvPolynomial.IsWeightedHomogeneous.add :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
{φ ψ : MvPolynomial σ R} {n : M} {w : σ → M},
MvPolynomial.IsWeightedHomogeneous w φ n →
MvPolynomial.IsWeightedHomogeneous w ψ n → MvPolynomial.IsWeightedHomogeneous w (φ + ψ) n
This theorem states that if you have two multivariate polynomials φ and ψ, both of which are weighted homogeneous of some weighted degree n, then their sum is also weighted homogeneous of the same weighted degree n. This holds in the context where the polynomials are over a commutative semiring (denoted by `R`), the weighted degrees are from an additively commutative monoid (denoted by `M`), and the weights are given by a function `w` mapping the variable indices to `M`. In other words, the property of being weighted homogeneous of a certain degree is preserved under addition of polynomials.
More concisely: If φ and ψ are multivariate polynomials over a commutative semiring with weighted degrees from an additively commutative monoid, and both are weighted homogeneous of degree n with respect to given weights, then their sum is also weighted homogeneous of degree n.
|
MvPolynomial.weightedTotalDegree_coe
theorem MvPolynomial.weightedTotalDegree_coe :
∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
[inst_2 : SemilatticeSup M] [inst_3 : OrderBot M] (w : σ → M) (p : MvPolynomial σ R),
p ≠ 0 → MvPolynomial.weightedTotalDegree' w p = ↑(MvPolynomial.weightedTotalDegree w p)
This theorem states that for any commutative semiring `R`, any set of variables `σ`, any additively commutative monoid `M` that is also both a semilattice with a supremum operation and a partially ordered set with a least element, and for any weight function `w` from `σ` to `M` and any nonzero multivariate polynomial `p` with coefficients in `R` and variables from `σ`, the weighted total degree of `p` calculated using the `weightedTotalDegree'` function, which may return a value in the extended nonnegative real numbers (represented by `WithBot M`), is actually a finite nonnegative real number and equals the weighted total degree of `p` calculated using the `weightedTotalDegree` function (which always returns a finite nonnegative real number). In other words, when `p` is nonzero, the potentially-infinite degree `weightedTotalDegree' w p` is actually finite and equals `weightedTotalDegree w p`.
More concisely: For any commutative semiring `R`, additively commutative monoid `M` with supremum and least element, weight function `w` from variables to `M`, and nonzero multivariate polynomial `p` with coefficients in `R` and variables from `σ`, the finite nonnegative real number `weightedTotalDegree w p` equals the finite nonnegative real number `weightedTotalDegree' w p`.
|