Isobaric polynomials

AbbreviationIsobaric weight of an exponent vector#✓fully proved

For a natural number \(k\) and an exponent vector \(\alpha = (\alpha_1, \dots, \alpha_k) \in \mathbb{N}^k\), the isobaric weight of \(\alpha\) is \(\sum_{j=1}^k j \alpha_j\).

The source's condition on the monomials of an isobaric polynomial of degree \(n\) is that this weight equals \(n\).

abbrev isobaricWeight {k : ℕ} (d : Fin k →₀ ℕ) : ℕ :=
  Finsupp.weight (fun j : Fin k ↦ j.val + 1) d

AbbreviationIsobaric polynomial#✓fully proved

Let \(k\) and \(n\) be natural numbers. A polynomial \(P \in \mathbb{Z}[t_1, \dots, t_k]\) is isobaric of degree \(n\) if every monomial \(t_1^{\alpha_1} \cdots t_k^{\alpha_k}\) occurring in \(P\) with nonzero coefficient satisfies \(\sum_{j=1}^k j \alpha_j = n\); that is, \(P\) is weighted homogeneous of degree \(n\) when the variable \(t_j\) has weight \(j\). In particular, the zero polynomial is isobaric of every degree.

abbrev IsIsobaric {k : ℕ} (n : ℕ) (P : MvPolynomial (Fin k) ℤ) : Prop :=
  MvPolynomial.IsWeightedHomogeneous (fun j : Fin k ↦ j.val + 1) P n

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.