Normalized coefficient matrices

The entry indexed by exponent vectors r and c is the coefficient of r + c, divided by its multinomial coefficient. Over a characteristic-zero field, when all queried exponents have degree d, a d-th power of a linear form gives an outer product. Row and column families may be arbitrary restrictions of the homogeneous exponent layers; no enumeration of all monomials is required.

Main definitions

• MvPolynomial.catalecticant: the normalized coefficient matrix, linear in the polynomial.

Main results

• MvPolynomial.catalecticant_linearCombination_pow: linear-form powers give outer products over a characteristic-zero field.

References

• The coefficient argument is adapted from LowerBound/Fusion/SumOfTerms/Waring.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.
• J. M. Landsberg and Z. Teitler, On the ranks and border ranks of symmetric tensors, equation (1) and Remark 6.5, describe the catalecticant bound.

theorem Finsupp.cast_multinomial_ne_zero {σ : Type u_1} {K : Type u_2} [AddMonoidWithOne K] [CharZero K] (s : σ →₀ ℕ) : ↑s.multinomial ≠ 0

Multinomial coefficients remain nonzero in characteristic zero.

noncomputable def MvPolynomial.catalecticant {σ : Type u_1} {K : Type u_2} {m : Type u_3} {n : Type u_4} [Field K] (rows : m → σ →₀ ℕ) (columns : n → σ →₀ ℕ) : MvPolynomial σ K →ₗ[K] Matrix m n K

Coefficients indexed by sums of row and column exponents, normalized by multinomials.

@[simp]

theorem MvPolynomial.catalecticant_apply {σ : Type u_1} {K : Type u_2} {m : Type u_3} {n : Type u_4} [Field K] (rows : m → σ →₀ ℕ) (columns : n → σ →₀ ℕ) (p : MvPolynomial σ K) (i : m) (j : n) : (catalecticant rows columns) p i j = p.coeff (rows i + columns j) / ↑(rows i + columns j).multinomial

The entry of the catalecticant of p at (i, j) is the coefficient of p at the exponent rows i + columns j, divided by the multinomial coefficient of that exponent.

theorem MvPolynomial.catalecticant_linearCombination_pow {σ : Type u_1} {K : Type u_2} {m : Type u_3} {n : Type u_4} [Field K] [Fintype σ] [CharZero K] (rows : m → σ →₀ ℕ) (columns : n → σ →₀ ℕ) (a : σ → K) (d : ℕ) (hdegree : ∀ (i : m) (j : n), ((rows i + columns j).sum fun (x : σ) (e : ℕ) => e) = d) : (catalecticant rows columns) ((∑ i : σ, a i • X i) ^ d) = Matrix.vecMulVec (fun (i : m) => (rows i).prod fun (v : σ) (e : ℕ) => a v ^ e) fun (j : n) => (columns j).prod fun (v : σ) (e : ℕ) => a v ^ e

A power of a linear form gives an outer product on any pair of exponent families whose combined degree is the power. The normalization is invertible in characteristic zero.