Catalecticant fusion for sums of powers

This module instantiates sum-of-terms fusion on actual multivariate polynomials. A charged term is a scalar multiple of a power of a linear form. The normalized middle catalecticant sends each such term to a rank-one matrix, while the squarefree monomial has a full-rank complement matrix.

References

The catalecticant rank bound is described in J. M. Landsberg and Zach Teitler, On the ranks and border ranks of symmetric tensors, equation (1) and Remark 6.5, arXiv:0901.0487. Here the middle flattening is restricted to squarefree row and column indices, and multinomial normalization is checked over any characteristic-zero field. The result is a power-term lower bound; it does not identify the exact Waring rank or formalize the paper's border-rank and singularity bounds.

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.exponent {ι : Type u_1} (set : Finset ι) : ι →₀ ℕ

Squarefree exponent vector associated to a finite set of variables.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.exponent set = Finsupp.indicator set fun (x : ι) (x_1 : x ∈ set) => 1

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.exponent_apply {ι : Type u_1} [DecidableEq ι] (set : Finset ι) (index : ι) : (exponent set) index = if index ∈ set then 1 else 0

theorem Algebraic.Fusion.SumOfTerms.Waring.exponent_sum {ι : Type u_1} (set : Finset ι) : ((exponent set).sum fun (x : ι) (multiplicity : ℕ) => multiplicity) = set.card

Total degree of a squarefree exponent is its set cardinality.

theorem Algebraic.Fusion.SumOfTerms.Waring.exponent_prod {ι : Type u_1} {K : Type u_2} [CommMonoid K] (coefficients : ι → K) (set : Finset ι) : ((exponent set).prod fun (index : ι) (multiplicity : ℕ) => coefficients index ^ multiplicity) = ∏ index ∈ set, coefficients index

Evaluating a squarefree exponent product gives the product over its set.

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.complement (n : ℕ) (set : MatrixRank.Layer (2 * n) n) : MatrixRank.Layer (2 * n) n

Complementing a middle-layer subset stays in the middle layer.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.complement n set = ⟨(↑set)ᶜ, ⋯⟩

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.complement_val (n : ℕ) (set : MatrixRank.Layer (2 * n) n) : ↑(complement n set) = (↑set)ᶜ

theorem Algebraic.Fusion.SumOfTerms.Waring.exponent_add_complement_eq_univ_iff (n : ℕ) (left right : MatrixRank.Layer (2 * n) n) : exponent ↑left + exponent ↑(complement n right) = exponent Finset.univ ↔ left = right

The complement-reindexed exponent sum is the all-ones exponent exactly on the diagonal.

theorem Algebraic.Fusion.SumOfTerms.Waring.exponent_add_complement_sum (n : ℕ) (left right : MatrixRank.Layer (2 * n) n) : ((exponent ↑left + exponent ↑(complement n right)).sum fun (x : Fin (2 * n)) (multiplicity : ℕ) => multiplicity) = 2 * n

Every complement-reindexed entry has total degree 2 * n.

structure Algebraic.Fusion.SumOfTerms.Waring.Term (K : Type) (n : ℕ) : Type

One scalar multiple of a power of a linear form.

• scale : K

  Scalar multiplying the power.

• coefficients : Fin (2 * n) → K

  Coefficients of the linear form in 2 * n variables.

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.linearForm {K : Type} [CommSemiring K] {n : ℕ} (term : Term K n) : MvPolynomial (Fin (2 * n)) K

Linear form represented by a term.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.linearForm term = ∑ index : Fin (2 * n), term.coefficients index • MvPolynomial.X index

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.termValue {K : Type} [CommSemiring K] {n : ℕ} (term : Term K n) : MvPolynomial (Fin (2 * n)) K

Polynomial value of a charged Waring term.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.termValue term = MvPolynomial.C term.scale * Algebraic.Fusion.SumOfTerms.Waring.linearForm term ^ (2 * n)

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.entryExponent (n : ℕ) (row column : MatrixRank.Layer (2 * n) n) : Fin (2 * n) →₀ ℕ

Exponent queried by one complement-reindexed catalecticant entry.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.catalecticant (K : Type) [Field K] (n : ℕ) : MvPolynomial (Fin (2 * n)) K →ₗ[K] Matrix (MatrixRank.Layer (2 * n) n) (MatrixRank.Layer (2 * n) n) K

Normalized middle catalecticant. Division by the multinomial coefficient makes powers of linear forms map to rank-one matrices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.catalecticant_apply {K : Type} [Field K] (n : ℕ) (polynomial : MvPolynomial (Fin (2 * n)) K) (row column : MatrixRank.Layer (2 * n) n) : (catalecticant K n) polynomial row column = polynomial.coeff (entryExponent n row column) / ↑(entryExponent n row column).multinomial

theorem Algebraic.Fusion.SumOfTerms.Waring.entryExponent_multinomial_ne_zero {K : Type} [Field K] [CharZero K] (n : ℕ) (row column : MatrixRank.Layer (2 * n) n) : ↑(entryExponent n row column).multinomial ≠ 0

The multinomial denominator of every queried entry is nonzero in characteristic zero.

theorem Algebraic.Fusion.SumOfTerms.Waring.entryExponent_prod {n : ℕ} {K : Type} [CommMonoid K] (coefficients : Fin (2 * n) → K) (row column : MatrixRank.Layer (2 * n) n) : ((entryExponent n row column).prod fun (index : Fin (2 * n)) (multiplicity : ℕ) => coefficients index ^ multiplicity) = (∏ index ∈ ↑row, coefficients index) * ∏ index ∈ ↑(complement n column), coefficients index

The coefficient product of an entry exponent factors across its row and complemented column.

theorem Algebraic.Fusion.SumOfTerms.Waring.coeff_linearForm_pow_entryExponent {n : ℕ} {K : Type} [CommSemiring K] (term : Term K n) (row column : MatrixRank.Layer (2 * n) n) : (linearForm term ^ (2 * n)).coeff (entryExponent n row column) = ↑(entryExponent n row column).multinomial * ((∏ index ∈ ↑row, term.coefficients index) * ∏ index ∈ ↑(complement n column), term.coefficients index)

Coefficient formula for a power of a linear form at a queried exponent.

def Algebraic.Fusion.SumOfTerms.Waring.leftVector {K : Type} [CommMonoid K] {n : ℕ} (term : Term K n) : MatrixRank.Layer (2 * n) n → K

Row vector in the rank-one catalecticant of a power term.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.leftVector term row = term.scale * ∏ index ∈ ↑row, term.coefficients index

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.rightVector {K : Type} [CommMonoid K] {n : ℕ} (term : Term K n) : MatrixRank.Layer (2 * n) n → K

Complement-reindexed column vector in the rank-one catalecticant.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.rightVector term column = ∏ index ∈ ↑(Algebraic.Fusion.SumOfTerms.Waring.complement n column), term.coefficients index

theorem Algebraic.Fusion.SumOfTerms.Waring.catalecticant_termValue {n : ℕ} {K : Type} [Field K] [CharZero K] (term : Term K n) : (catalecticant K n) (termValue term) = Matrix.vecMulVec (leftVector term) (rightVector term)

The normalized catalecticant of a power term is an outer product.

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.targetExponent (n : ℕ) : Fin (2 * n) →₀ ℕ

All-ones exponent of the squarefree target monomial.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.targetExponent n = Algebraic.Fusion.SumOfTerms.Waring.exponent Finset.univ

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.target (K : Type) [CommSemiring K] (n : ℕ) : MvPolynomial (Fin (2 * n)) K

Product of all 2 * n variables, represented as a monomial.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.target K n = (MvPolynomial.monomial (Algebraic.Fusion.SumOfTerms.Waring.targetExponent n)) 1

theorem Algebraic.Fusion.SumOfTerms.Waring.target_eq_prod_X (K : Type) [CommSemiring K] (n : ℕ) : target K n = ∏ index : Fin (2 * n), MvPolynomial.X index

The target definition is literally the product of all variables.

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.targetScalar (K : Type) [Field K] (n : ℕ) : K

The inverse, in K, of the multinomial coefficient of the target exponent; it appears on the diagonal of the normalized target catalecticant. It is nonzero in characteristic zero (targetScalar_ne_zero).

Equations

• Algebraic.Fusion.SumOfTerms.Waring.targetScalar K n = (↑(Algebraic.Fusion.SumOfTerms.Waring.targetExponent n).multinomial)⁻¹

theorem Algebraic.Fusion.SumOfTerms.Waring.targetScalar_ne_zero {K : Type} [Field K] [CharZero K] (n : ℕ) : targetScalar K n ≠ 0

The target normalizing scalar is nonzero in characteristic zero.

theorem Algebraic.Fusion.SumOfTerms.Waring.catalecticant_target {K : Type} [Field K] (n : ℕ) : (catalecticant K n) (target K n) = targetScalar K n • 1

The squarefree target has a scalar identity middle catalecticant.

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.feature (K : Type) [Field K] (n : ℕ) : MvPolynomial (Fin (2 * n)) K →ₗ[K] (MatrixRank.Layer (2 * n) n → K) →ₗ[K] MatrixRank.Layer (2 * n) n → K

Catalecticant followed by the matrix-to-linear-map equivalence.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.feature K n = ↑Matrix.toLin' ∘ₗ Algebraic.Fusion.SumOfTerms.Waring.catalecticant K n

theorem Algebraic.Fusion.SumOfTerms.Waring.feature_target {K : Type} [Field K] (n : ℕ) : (feature K n) (target K n) = targetScalar K n • LinearMap.id

Feature of the target is targetScalar K n times the identity map, over any field. The scalar is nonzero in characteristic zero (targetScalar_ne_zero).

theorem Algebraic.Fusion.SumOfTerms.Waring.target_rank_ge {K : Type} [Field K] [CharZero K] (n : ℕ) : ↑n.centralBinom ≤ ((feature K n) (target K n)).rank

The target feature has full middle-layer rank.

theorem Algebraic.Fusion.SumOfTerms.Waring.term_rank_le_one {n : ℕ} {K : Type} [Field K] [CharZero K] (term : Term K n) : ((feature K n) (termValue term)).rank ≤ 1

Every charged power term has feature rank at most one.

@[reducible, inline]

noncomputable abbrev Algebraic.Fusion.SumOfTerms.Waring.problem (K : Type) [CommSemiring K] (n : ℕ) : Problem (MvPolynomial (Fin (2 * n)) K)

Construct the squarefree monomial from power terms, with no free inputs.

Equations

• Algebraic.Fusion.SumOfTerms.Waring.problem K n = { inputCount := 0, inputs := fun (input : Fin 0) => input.elim0, target := Algebraic.Fusion.SumOfTerms.Waring.target K n }

noncomputable def Algebraic.Fusion.SumOfTerms.Waring.certificate (K : Type) [Field K] [CharZero K] (n : ℕ) : RankCertificate termValue (problem K n)

Full rank certificate for the squarefree target against powers of linear forms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.certificate_targetRank (K : Type) [Field K] [CharZero K] (n : ℕ) : (certificate K n).targetRank = n.centralBinom

@[simp]

theorem Algebraic.Fusion.SumOfTerms.Waring.certificate_termRank (K : Type) [Field K] [CharZero K] (n : ℕ) : (certificate K n).termRank = 1

theorem Algebraic.Fusion.SumOfTerms.Waring.centralBinom_lowerBound {K : Type} [Field K] [CharZero K] (n : ℕ) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 1) (constructs : (problem K n).Constructs circuit (SumOfTerms.interpretation termValue)) : n.centralBinom ≤ circuit.cost SumOfTerms.termCost

The squarefree monomial in 2 * n variables requires at least the central binomial number of power terms in a sum-of-powers circuit.

theorem Algebraic.Fusion.SumOfTerms.Waring.four_pow_lt_mul_cost {K : Type} [Field K] [CharZero K] (n : ℕ) (n_big : 4 ≤ n) (circuit : Circuit (SumOfTerms.signature (Term K n)) 0 1) (constructs : (problem K n).Constructs circuit (SumOfTerms.interpretation termValue)) : 4 ^ n < n * circuit.cost SumOfTerms.termCost

Explicit exponential lower bound for squarefree-monomial sum-of-powers circuits.