Applying the squarefree-monomial Waring bound #
A finite sum of scaled 2n-th powers of linear forms representing the product
of 2n variables has at least choose (2n) n terms. The premise is an equality
of polynomials; callers do not need to encode the sum as a circuit.
This is a lower bound on the number of power terms in this restricted
representation, not on unrestricted arithmetic circuit size.
For the source correspondence of the catalecticant argument, see the
module documentation of Algebraic.LowerBound.Fusion.SumOfTerms.Waring.
theorem
Algebraic.Applications.waringSum_lowerBound
{K : Type}
[Field K]
[CharZero K]
{ι : Type u_1}
(n : ℕ)
(indices : Finset ι)
(scale : ι → K)
(coefficients : ι → Fin (2 * n) → K)
(represents :
∑ i ∈ indices,
MvPolynomial.C (scale i) * (∑ j : Fin (2 * n), MvPolynomial.C (coefficients i j) * MvPolynomial.X j) ^ (2 * n) = ∏ j : Fin (2 * n), MvPolynomial.X j)
:
A sum of scaled powers representing the squarefree monomial needs at least the central binomial number of terms, over any characteristic-zero field.