Set-multilinear polynomials

The variables σ of a polynomial are split into d blocks by a map blk : σ → Fin d. A choice of one variable from each block in a set S of blocks (MvPolynomial.BlockChoice) determines the monomial MvPolynomial.blockMonomial that multiplies the chosen variables. Distinct choices give distinct monomials (MvPolynomial.blockMonomial_injective), so the choices on S enumerate the set-multilinear monomials on S, and there are ∏ i ∈ S, |block i| of them (MvPolynomial.card_blockChoice). A polynomial is set-multilinear on S (MvPolynomial.IsSetMultilinear) when every monomial in its support has this form: it takes exactly one variable, with exponent one, from each block in S, and no variable from any other block.

Set-multilinear polynomials are closed under sums and scaling on a fixed set of blocks, and under products over disjoint sets of blocks. A coefficient of such a product on a monomial that splits along the blocks is the product of the coefficients of the two parts (MvPolynomial.coeff_mul_blockMonomial); this is what makes the coefficient matrix of a product a Kronecker product.

Main definitions

• MvPolynomial.BlockChoice, MvPolynomial.blockMonomial: choices of one variable per block and their monomials.
• MvPolynomial.IsSetMultilinear: set-multilinear polynomials on a set of blocks.

Main results

• MvPolynomial.blockMonomial_injective, MvPolynomial.card_blockChoice: the choices on S are in bijection with the set-multilinear monomials on S, which they count.
• MvPolynomial.IsSetMultilinear.add, .smul, .mul, .sum, .prod, .one, MvPolynomial.isSetMultilinear_C, MvPolynomial.isSetMultilinear_X: closure properties.
• MvPolynomial.coeff_mul_blockMonomial: coefficients of a product of set-multilinear polynomials on disjoint blocks.

References

• N. Limaye, S. Srinivasan, S. Tavenas, Superpolynomial lower bounds against low-depth algebraic circuits, §1, p. 2 (set-multilinear polynomials) and §2.1, p. 6 (the sets M^P_w, M^N_w of set-multilinear monomials). The encoding by block maps and choices is original.

@[reducible, inline]

abbrev MvPolynomial.BlockChoice {σ : Type u_1} {d : ℕ} (blk : σ → Fin d) (S : Finset (Fin d)) : Type u_1

A choice of one variable from each block in S.

def MvPolynomial.BlockChoice.restrict {σ : Type u_1} {d : ℕ} {blk : σ → Fin d} {S T : Finset (Fin d)} (hTS : T ⊆ S) (x : BlockChoice blk S) : BlockChoice blk T

Restrict a choice on S to a subset T of its blocks.

noncomputable def MvPolynomial.blockMonomial {σ : Type u_1} {d : ℕ} (blk : σ → Fin d) (S : Finset (Fin d)) (x : BlockChoice blk S) : σ →₀ ℕ

The exponent vector of the product of the variables chosen by x.

theorem MvPolynomial.blockMonomial_apply {σ : Type u_1} {d : ℕ} [DecidableEq σ] (blk : σ → Fin d) (S : Finset (Fin d)) (x : BlockChoice blk S) (v : σ) : (blockMonomial blk S x) v = if h : blk v ∈ S then if ↑(x ⟨blk v, h⟩) = v then 1 else 0 else 0

The monomial of a choice has exponent 1 at the chosen variable of each block in S, and 0 elsewhere.

theorem MvPolynomial.blockMonomial_apply_of_notMem {σ : Type u_1} {d : ℕ} (blk : σ → Fin d) {S : Finset (Fin d)} (x : BlockChoice blk S) {v : σ} (hv : blk v ∉ S) : (blockMonomial blk S x) v = 0

A variable outside the blocks of S does not occur in the monomial of a choice on S.

theorem MvPolynomial.blockMonomial_apply_of_eq {σ : Type u_1} {d : ℕ} [DecidableEq σ] {blk : σ → Fin d} {S : Finset (Fin d)} (x : BlockChoice blk S) {i : ↥S} {v : σ} (hv : blk v = ↑i) : (blockMonomial blk S x) v = if ↑(x i) = v then 1 else 0

At a variable of block i, the monomial of a choice has exponent 1 if the variable is the one chosen in block i, and 0 otherwise.

theorem MvPolynomial.blockMonomial_injective {σ : Type u_1} {d : ℕ} (blk : σ → Fin d) (S : Finset (Fin d)) : Function.Injective (blockMonomial blk S)

Distinct choices give distinct monomials, so the choices on S are in bijection with the set-multilinear monomials on S, the set M^P_w or M^N_w of [LimayeSrinivasanTavenas2021, §2.1] for S the positive or negative blocks; card_blockChoice therefore counts these monomials.

theorem MvPolynomial.blockMonomial_restrict_apply {σ : Type u_1} {d : ℕ} (blk : σ → Fin d) {S T : Finset (Fin d)} (hTS : T ⊆ S) (x : BlockChoice blk S) (v : σ) : (blockMonomial blk T (BlockChoice.restrict hTS x)) v = if blk v ∈ T then (blockMonomial blk S x) v else 0

Restricting a choice to a subset of the blocks restricts its monomial to those blocks.

theorem MvPolynomial.blockMonomial_inter_apply {σ : Type u_1} {d : ℕ} (blk : σ → Fin d) {A : Finset (Fin d)} (S : Finset (Fin d)) (x : BlockChoice blk A) (v : σ) : (blockMonomial blk (A ∩ S) (BlockChoice.restrict ⋯ x)) v = if blk v ∈ S then (blockMonomial blk A x) v else 0

Restricting a choice on A to the blocks of A ∩ S restricts its monomial to the blocks of S.

theorem MvPolynomial.card_blockChoice {σ : Type u_1} {d : ℕ} [Fintype σ] (blk : σ → Fin d) (S : Finset (Fin d)) : Fintype.card (BlockChoice blk S) = ∏ i ∈ S, Fintype.card { x : σ // blk x = i }

There are ∏ i ∈ S, |block i| choices of one variable per block of S.

theorem MvPolynomial.card_blockChoice_inter_mul {σ : Type u_1} {d : ℕ} [Fintype σ] (blk : σ → Fin d) {A S T : Finset (Fin d)} (hST : Disjoint S T) (hA : A ⊆ S ∪ T) : Fintype.card (BlockChoice blk A) = Fintype.card (BlockChoice blk (A ∩ S)) * Fintype.card (BlockChoice blk (A ∩ T))

The choices on A split into choices on A ∩ S and A ∩ T when S and T are disjoint and cover A.

def MvPolynomial.IsSetMultilinear {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (S : Finset (Fin d)) (f : MvPolynomial σ K) : Prop

A polynomial is set-multilinear on the set S of blocks if every monomial in its support is the product of one variable from each block in S: it has exactly one variable, with exponent one, from each block in S, and no variable from any other block.

theorem MvPolynomial.IsSetMultilinear.apply_eq_zero {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S : Finset (Fin d)} {f : MvPolynomial σ K} (hf : IsSetMultilinear blk S f) {m : σ →₀ ℕ} (hm : m ∈ f.support) {v : σ} (hv : blk v ∉ S) : m v = 0

A monomial in the support of a set-multilinear polynomial on S has no variable outside the blocks of S.

theorem MvPolynomial.IsSetMultilinear.zero {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S : Finset (Fin d)} : IsSetMultilinear blk S 0

The zero polynomial is set-multilinear on every set of blocks.

theorem MvPolynomial.IsSetMultilinear.add {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S : Finset (Fin d)} {f g : MvPolynomial σ K} (hf : IsSetMultilinear blk S f) (hg : IsSetMultilinear blk S g) : IsSetMultilinear blk S (f + g)

A sum of set-multilinear polynomials on S is set-multilinear on S.

theorem MvPolynomial.IsSetMultilinear.smul {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S : Finset (Fin d)} {f : MvPolynomial σ K} (c : K) (hf : IsSetMultilinear blk S f) : IsSetMultilinear blk S (c • f)

A scalar multiple of a set-multilinear polynomial on S is set-multilinear on S.

theorem MvPolynomial.IsSetMultilinear.mul {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S T : Finset (Fin d)} {f g : MvPolynomial σ K} (hf : IsSetMultilinear blk S f) (hg : IsSetMultilinear blk T g) (hST : Disjoint S T) : IsSetMultilinear blk (S ∪ T) (f * g)

A product of set-multilinear polynomials on disjoint sets of blocks is set-multilinear on their union.

theorem MvPolynomial.isSetMultilinear_C {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (c : K) : IsSetMultilinear blk ∅ (C c)

A constant is set-multilinear on the empty set of blocks.

theorem MvPolynomial.isSetMultilinear_X {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (v : σ) : IsSetMultilinear blk {blk v} (X v)

A variable is set-multilinear on its own block.

theorem MvPolynomial.IsSetMultilinear.one {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) : IsSetMultilinear blk ∅ 1

The constant 1 is set-multilinear on the empty set of blocks.

theorem MvPolynomial.IsSetMultilinear.sum {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S : Finset (Fin d)} {ι : Type u_3} (s : Finset ι) {f : ι → MvPolynomial σ K} (hf : ∀ i ∈ s, IsSetMultilinear blk S (f i)) : IsSetMultilinear blk S (∑ i ∈ s, f i)

A finite sum of set-multilinear polynomials on S is set-multilinear on S.

theorem MvPolynomial.IsSetMultilinear.prod {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {ι : Type u_3} (s : Finset ι) {f : ι → MvPolynomial σ K} {T : ι → Finset (Fin d)} (hT : (↑s).PairwiseDisjoint T) (hf : ∀ i ∈ s, IsSetMultilinear blk (T i) (f i)) : IsSetMultilinear blk (s.biUnion T) (∏ i ∈ s, f i)

A finite product of set-multilinear polynomials on pairwise disjoint sets of blocks is set-multilinear on their union.

theorem MvPolynomial.coeff_mul_blockMonomial {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {A B S T : Finset (Fin d)} {f g : MvPolynomial σ K} (hf : IsSetMultilinear blk S f) (hg : IsSetMultilinear blk T g) (hST : Disjoint S T) (hA : A ⊆ S ∪ T) (hB : B ⊆ S ∪ T) (r : BlockChoice blk A) (c : BlockChoice blk B) : (f * g).coeff (blockMonomial blk A r + blockMonomial blk B c) = f.coeff (blockMonomial blk (A ∩ S) (BlockChoice.restrict ⋯ r) + blockMonomial blk (B ∩ S) (BlockChoice.restrict ⋯ c)) * g.coeff (blockMonomial blk (A ∩ T) (BlockChoice.restrict ⋯ r) + blockMonomial blk (B ∩ T) (BlockChoice.restrict ⋯ c))

The product of set-multilinear polynomials on disjoint blocks: a coefficient of f * g on a monomial that splits along the blocks is the product of the coefficients of its two parts.