Set-multilinear formulas compute set-multilinear polynomials

A formula of unbounded fan-in that is set-multilinear on a set S of blocks (Cslib.Circuits.Arithmetic.SPFormula.IsSetMultilinear, a syntactic condition on the formula) computes a polynomial that is set-multilinear on S (MvPolynomial.IsSetMultilinear, a condition on its support), so the relative-rank bounds of [LST21] apply to it. The proof is by induction on the formula predicate: inputs and constants are set-multilinear on their own block and on no block, sum gates are closed under scaling and sums, and product gates under products over pairwise disjoint sets of blocks.

Main results

• Cslib.Circuits.Arithmetic.SPFormula.IsSetMultilinear.isSetMultilinear_polynomial: a set-multilinear formula on S computes a set-multilinear polynomial on S.

References

• N. Limaye, S. Srinivasan, S. Tavenas, Superpolynomial lower bounds against low-depth algebraic circuits, §1, p. 2, define set-multilinear circuits semantically, by the polynomials their gates compute, so for them the statement here holds by definition. The syntactic predicate SPFormula.IsSetMultilinear strengthens that definition; the statement and proof here, which connect the two, are original.

theorem Cslib.Circuits.Arithmetic.SPFormula.IsSetMultilinear.isSetMultilinear_polynomial {K : Type u_1} [CommSemiring K] {n d : ℕ} {blk : Fin n → Fin d} {F : SPFormula K n} {S : Finset (Fin d)} (h : IsSetMultilinear blk F S) : MvPolynomial.IsSetMultilinear blk S F.polynomial

A formula that is set-multilinear on the set S of blocks computes a polynomial that is set-multilinear on S (original).