The set-multilinear projection of a product, by set partitions

For a product ∏ j, f j of polynomials, MvPolynomial.smProj_prod writes the part on a set S of blocks as a sum over the ordered splits of S into one part for each factor. A factor that gets the empty part contributes its constant term, so grouping the splits by their nonempty parts writes it as a sum over the set partitions P of S and the injections e of the parts of P into the factors (MvPolynomial.smProj_prod_eq_sum_finpartition):

π_S(∏ j, f j) = ∑_P ∑_{e : P ↪ ι} ∏_{T ∈ P} π_T(f (e T)) · ∏_{j ∉ im e} f_j(0).

Over a field, let Z be the set of factors with constant term 0. Dividing each factor outside Z by its constant term turns the inner sum into a rectangular permanent restricted to the injections whose image contains Z (Matrix.rectPermSurj), and the Binet–Minc identity with inclusion–exclusion (Matrix.rectPermSurj_eq_sum_sign_prod_sameCycle) expands it as a signed sum over the permutations of the parts of P and the subsets of Z (MvPolynomial.smProj_prod_eq_sum_sign). This is the expansion of the proof of [Forbes2024, Lemma 26], pp. 31:13–31:14, with inclusion–exclusion in place of [Forbes2024, Lemma 21] (p. 31:12) and the permutation form of the Binet–Minc identity in place of its partition form [Forbes2024, Theorem 13] (p. 31:10). Its number of products of sums is bounded in terms of #S and #Z only, not of the number of factors. If #S < #Z the part is 0 (MvPolynomial.smProj_prod_eq_zero_of_card_lt).

Main results

• MvPolynomial.smProj_prod_eq_sum_finpartition: the part of a product, by set partitions.
• MvPolynomial.smProj_prod_eq_zero_of_card_lt: it vanishes when more than #S factors have constant term 0.
• MvPolynomial.smProj_prod_eq_sum_sign: the part of a product over a field, by the Binet–Minc identity.

References

• M. A. Forbes, Low-depth algebraic circuit lower bounds over any field, proof of Lemma 26, pp. 31:13–31:14, which collects the set-multilinear terms of a product by set partitions and injections and writes them as surjective permanents. The statements here as identities of polynomials, the normalization by the constant terms in this form and the use of inclusion–exclusion and of the permutation form of the Binet–Minc identity are original.

theorem MvPolynomial.smProj_prod_eq_sum_finpartition {σ : Type u_1} {K : Type u_2} {ι : Type u_3} {d : ℕ} [Fintype ι] [DecidableEq ι] [CommSemiring K] (blk : σ → Fin d) (S : Finset (Fin d)) (f : ι → MvPolynomial σ K) : (smProj blk S) (∏ j : ι, f j) = ∑ P : Finpartition S, ∑ e : ↥P.parts ↪ ι, (∏ r : ↥P.parts, (smProj blk ↑r) (f (e r))) * ∏ j ∈ (Finset.map e Finset.univ)ᶜ, C (constantCoeff (f j))

The part of a product, by set partitions (original as stated; the collection of terms in the proof of [Forbes2024, Lemma 26], p. 31:14): the part on S of ∏ j, f j is the sum over the set partitions P of S and the injections e of the parts of P into the factors of the product of the parts π_T(f (e T)), times the constant terms of the factors outside the image of e.

theorem MvPolynomial.smProj_prod_eq_zero_of_card_lt {σ : Type u_1} {K : Type u_2} {ι : Type u_3} {d : ℕ} [Fintype ι] [CommSemiring K] (blk : σ → Fin d) {S : Finset (Fin d)} (f : ι → MvPolynomial σ K) {Z : Finset ι} (hZ : ∀ j ∈ Z, constantCoeff (f j) = 0) (h : S.card < Z.card) : (smProj blk S) (∏ j : ι, f j) = 0

The part of a product vanishes when too many factors vanish at 0 (original): if more than #S factors have constant term 0, the part on S of the product is 0.

theorem MvPolynomial.smProj_prod_eq_sum_sign {σ : Type u_1} {K : Type u_2} {ι : Type u_3} {d : ℕ} [Fintype ι] [DecidableEq ι] [Field K] (blk : σ → Fin d) (S : Finset (Fin d)) (f : ι → MvPolynomial σ K) {Z : Finset ι} (hZ : ∀ (j : ι), j ∈ Z ↔ constantCoeff (f j) = 0) {u : ι → K} (hu₀ : ∀ j ∈ Z, u j = 1) (hu : ∀ j ∉ Z, u j * constantCoeff (f j) = 1) : (smProj blk S) (∏ j : ι, f j) = C (∏ j ∈ Zᶜ, constantCoeff (f j)) * ∑ P : Finpartition S, ∑ π : Equiv.Perm ↥P.parts, C ↑↑(Equiv.Perm.sign π) * ∑ Y ∈ Z.powerset, C ((-1) ^ Y.card) * ∏ q : Quotient (Equiv.Perm.SameCycle.setoid π), ∑ j ∈ Yᶜ, C (u j ^ {r : ↥P.parts | ⟦r⟧ = q}.card) * ∏ r : ↥P.parts with ⟦r⟧ = q, (smProj blk ↑r) (f j)

The part of a product over a field, by the Binet–Minc identity (original as stated; the expansion of the proof of [Forbes2024, Lemma 26], pp. 31:13–31:14, with inclusion–exclusion in place of [Forbes2024, Lemma 21] and the permutation form of the Binet–Minc identity in place of [Forbes2024, Theorem 13], p. 31:10). Let Z be the set of factors with constant term 0, and let u j be the inverse of the constant term of f j for j ∉ Z and 1 for j ∈ Z. Then the part on S of ∏ j, f j is the product of the nonzero constant terms times the sum, over the set partitions P of S, the permutations π of the parts of P and the subsets Y ⊆ Z, of sgn π (-1) ^ #Y times the product over the orbits q of π of ∑_{j ∉ Y} u j ^ #q ∏_{T ∈ q} π_T(f j).