Complete homogeneous values at constant sequences

At the constant power-sum sequence m the complete homogeneous values are the binomial coefficients C(m+d−1, d) (the generating function (1−z)^{−m}); at −m they are the signed binomials (−1)^d C(m, d) (the generating function (1−z)^m). These feed the tensor-space traces of the dimension-bound argument.

theorem RS.newtonH_const (m d : ℕ) : newtonH (fun (x : ℕ) => ↑m) d = ↑((m + d - 1).choose d)

Complete homogeneous values at the constant sequence are binomial coefficients.

theorem RS.newtonH_neg_const (m : ℕ) (hm : 1 ≤ m) (d : ℕ) : newtonH (fun (x : ℕ) => -↑m) d = (-1) ^ d * ↑(m.choose d)

Complete homogeneous values at the negated constant sequence are signed binomials.