Relative rank

The variables σ of a polynomial are split into d blocks by a map blk : σ → Fin d, and set-multilinear polynomials and their monomials are described by choices of one variable per block (MvPolynomial.BlockChoice, MvPolynomial.IsSetMultilinear).

For sets A and B of blocks, the relative-rank matrix relMatrix blk A B f has rows indexed by choices on A and columns by choices on B; its entry is the coefficient in f of the product of the two monomials. The relative rank relRank blk A B f is its rank divided by the geometric mean √(rows * columns) of its dimensions. With A the positive and B the negative blocks of a word w, and block i of size 2 ^ |w i|, this is the measure relrk_w of Limaye, Srinivasan and Tavenas [LimayeSrinivasanTavenas2021, §2.1, p. 6]; general A and B also express the restricted measures relrk_{w|S} used in the multiplicativity property.

The sets A and B are meant to be disjoint, as the positive and negative blocks of a word are. The definitions do not require it: on a block of A ∩ B the product of a row and a column monomial can have exponent 2, and the entries are then coefficients of monomials that are not set-multilinear. The results below hold for arbitrary A and B.

This file proves the bound relrk_w ≤ 1 of the display defining relrk_w (relRank_le_one) and the three properties of Claim 7 (ECCC TR21-081, Revision 1, §2.1, pp. 6–7):

• imbalance: relRank_le_sqrt_rows_div_cols and relRank_le_sqrt_cols_div_rows bound the relative rank by the square root of the ratio of the two dimensions, in both orders; together they bound it by the square root of the smaller dimension over the larger, which is Claim 7(1);
• subadditivity: relRank_add_le, Claim 7(2);
• multiplicativity: relRank_mul_le for two factors and relRank_prod_le for a finite product, for set-multilinear factors on pairwise disjoint sets of blocks, Claim 7(3). LST state equality; only the inequality is proved here, which is the direction their lower bound uses.

The rank-level statements rank_relMatrix_sq_le, rank_relMatrix_add_le and rank_relMatrix_mul_le are natural-number forms of relrk_w ≤ 1, subadditivity and multiplicativity. The dimensions are counted by MvPolynomial.card_blockChoice.

Main definitions

• Cslib.Circuits.Arithmetic.relMatrix: the relative-rank coefficient matrix.
• Cslib.Circuits.Arithmetic.relRank: the normalized relative rank, a real number.
• Cslib.Circuits.Arithmetic.blockChoiceCongr: a renaming of the variables along their blocks, acting on choices of one variable per block.

Main results

• Cslib.Circuits.Arithmetic.relRank_le_one: the relative rank is at most 1.
• Cslib.Circuits.Arithmetic.relRank_le_sqrt_rows_div_cols, Cslib.Circuits.Arithmetic.relRank_le_sqrt_cols_div_rows: imbalance.
• Cslib.Circuits.Arithmetic.relRank_add_le: subadditivity.
• Cslib.Circuits.Arithmetic.relRank_smul_le, relRank_smul: scalar multiples.
• Cslib.Circuits.Arithmetic.relRank_mul_le, Cslib.Circuits.Arithmetic.relRank_prod_le: multiplicativity, as an inequality.
• Cslib.Circuits.Arithmetic.relMatrix_rename, Cslib.Circuits.Arithmetic.relRank_rename: renaming the variables along their blocks permutes the rows and columns, and keeps the relative rank.

References

• N. Limaye, S. Srinivasan, S. Tavenas, Superpolynomial lower bounds against low-depth algebraic circuits, §2.1, pp. 6–7, Claim 7. Parametrizing the measure by a block map and two arbitrary sets of blocks, instead of by a word, and its invariance under renaming, are original to this formalization.

noncomputable def Cslib.Circuits.Arithmetic.relMatrix {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (A B : Finset (Fin d)) (f : MvPolynomial σ K) : Matrix (MvPolynomial.BlockChoice blk A) (MvPolynomial.BlockChoice blk B) K

The relative-rank matrix of f for the row blocks A and column blocks B: rows are indexed by choices of one variable in each block of A, columns by choices on B, and the entry is the coefficient in f of the product of the two monomials. With A and B the positive and negative blocks of a word, this is the matrix M_w(f) of [LimayeSrinivasanTavenas2021, §2.1, p. 6]; indexing it by two arbitrary sets of blocks, so that it also covers LST's sub-words w|S, is original. A and B are meant to be disjoint: on a shared block the product monomial can have exponent 2, and the entries are then coefficients of non-set-multilinear monomials.

@[simp]

theorem Cslib.Circuits.Arithmetic.relMatrix_apply {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (A B : Finset (Fin d)) (f : MvPolynomial σ K) (r : MvPolynomial.BlockChoice blk A) (c : MvPolynomial.BlockChoice blk B) : relMatrix blk A B f r c = f.coeff (MvPolynomial.blockMonomial blk A r + MvPolynomial.blockMonomial blk B c)

The entry of the relative-rank matrix at the row choice r and the column choice c is the coefficient of the product of their monomials.

@[simp]

theorem Cslib.Circuits.Arithmetic.relMatrix_zero {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (A B : Finset (Fin d)) : relMatrix blk A B 0 = 0

The relative-rank matrix of 0 is 0.

theorem Cslib.Circuits.Arithmetic.relMatrix_add {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (A B : Finset (Fin d)) (f g : MvPolynomial σ K) : relMatrix blk A B (f + g) = relMatrix blk A B f + relMatrix blk A B g

The relative-rank matrix is additive in the polynomial.

theorem Cslib.Circuits.Arithmetic.relMatrix_smul {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (A B : Finset (Fin d)) (c : K) (f : MvPolynomial σ K) : relMatrix blk A B (c • f) = c • relMatrix blk A B f

The relative-rank matrix commutes with scaling.

theorem Cslib.Circuits.Arithmetic.relMatrix_mul {σ : 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 : MvPolynomial.IsSetMultilinear blk S f) (hg : MvPolynomial.IsSetMultilinear blk T g) (hST : Disjoint S T) (hA : A ⊆ S ∪ T) (hB : B ⊆ S ∪ T) : relMatrix blk A B (f * g) = (Matrix.kroneckerMap (fun (x1 x2 : K) => x1 * x2) (relMatrix blk (A ∩ S) (B ∩ S) f) (relMatrix blk (A ∩ T) (B ∩ T) g)).submatrix (fun (r : MvPolynomial.BlockChoice blk A) => (MvPolynomial.BlockChoice.restrict ⋯ r, MvPolynomial.BlockChoice.restrict ⋯ r)) fun (c : MvPolynomial.BlockChoice blk B) => (MvPolynomial.BlockChoice.restrict ⋯ c, MvPolynomial.BlockChoice.restrict ⋯ c)

The relative-rank matrix of a product of set-multilinear polynomials on disjoint blocks is a submatrix of the Kronecker product of the factors' matrices.

Renaming the variables along their blocks

def Cslib.Circuits.Arithmetic.blockChoiceCongr {σ : Type u_1} {d : ℕ} {τ : Type u_3} {blk : σ → Fin d} {blk' : τ → Fin d} (e : σ ≃ τ) (he : ∀ (x : σ), blk' (e x) = blk x) (S : Finset (Fin d)) : MvPolynomial.BlockChoice blk S ≃ MvPolynomial.BlockChoice blk' S

A renaming of the variables that respects the blocks maps choices of one variable per block to choices of one variable per block.

@[simp]

theorem Cslib.Circuits.Arithmetic.blockChoiceCongr_symm_apply_coe {σ : Type u_1} {d : ℕ} {τ : Type u_3} {blk : σ → Fin d} {blk' : τ → Fin d} (e : σ ≃ τ) (he : ∀ (x : σ), blk' (e x) = blk x) (S : Finset (Fin d)) (y : MvPolynomial.BlockChoice blk' S) (i : ↥S) : ↑((blockChoiceCongr e he S).symm y i) = e.symm ↑(y i)

@[simp]

theorem Cslib.Circuits.Arithmetic.blockChoiceCongr_apply_coe {σ : Type u_1} {d : ℕ} {τ : Type u_3} {blk : σ → Fin d} {blk' : τ → Fin d} (e : σ ≃ τ) (he : ∀ (x : σ), blk' (e x) = blk x) (S : Finset (Fin d)) (x : MvPolynomial.BlockChoice blk S) (i : ↥S) : ↑((blockChoiceCongr e he S) x i) = e ↑(x i)

theorem Cslib.Circuits.Arithmetic.blockMonomial_blockChoiceCongr {σ : Type u_1} {d : ℕ} {τ : Type u_3} {blk : σ → Fin d} {blk' : τ → Fin d} (e : σ ≃ τ) (he : ∀ (x : σ), blk' (e x) = blk x) (S : Finset (Fin d)) (x : MvPolynomial.BlockChoice blk S) : MvPolynomial.blockMonomial blk' S ((blockChoiceCongr e he S) x) = Finsupp.mapDomain (⇑e) (MvPolynomial.blockMonomial blk S x)

The monomial of a renamed choice is the renamed monomial.

theorem Cslib.Circuits.Arithmetic.relMatrix_rename {σ : Type u_1} {K : Type u_2} {d : ℕ} {τ : Type u_3} {blk : σ → Fin d} {blk' : τ → Fin d} [CommSemiring K] (e : σ ≃ τ) (he : ∀ (x : σ), blk' (e x) = blk x) (A B : Finset (Fin d)) (f : MvPolynomial σ K) : relMatrix blk' A B ((MvPolynomial.rename ⇑e) f) = (relMatrix blk A B f).submatrix ⇑(blockChoiceCongr e he A).symm ⇑(blockChoiceCongr e he B).symm

The relative-rank matrix of a renamed polynomial is the relative-rank matrix of the polynomial, with rows and columns renamed.

noncomputable def Cslib.Circuits.Arithmetic.relRank {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] (blk : σ → Fin d) (A B : Finset (Fin d)) (f : MvPolynomial σ K) : ℝ

Relative rank ([LimayeSrinivasanTavenas2021, §2.1, p. 6]): the rank of the relative-rank matrix divided by the geometric mean of its dimensions. As for relMatrix, the row and column blocks A and B are meant to be disjoint.

theorem Cslib.Circuits.Arithmetic.relRank_nonneg {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] (blk : σ → Fin d) (A B : Finset (Fin d)) (f : MvPolynomial σ K) : 0 ≤ relRank blk A B f

The relative rank is nonnegative.

@[simp]

theorem Cslib.Circuits.Arithmetic.relRank_zero {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] (blk : σ → Fin d) (A B : Finset (Fin d)) : relRank blk A B 0 = 0

The zero polynomial has relative rank 0.

theorem Cslib.Circuits.Arithmetic.rank_relMatrix_sq_le {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] (blk : σ → Fin d) (A B : Finset (Fin d)) (f : MvPolynomial σ K) : (relMatrix blk A B f).rank ^ 2 ≤ Fintype.card (MvPolynomial.BlockChoice blk A) * Fintype.card (MvPolynomial.BlockChoice blk B)

The relative rank is at most one, square form: the square of the rank is at most the product of the dimensions. This is the natural-number form of the bound relrk_w ≤ 1 in the display defining relrk_w in [LimayeSrinivasanTavenas2021, §2.1, p. 6].

theorem Cslib.Circuits.Arithmetic.relRank_le_sqrt_rows_div_cols {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] (blk : σ → Fin d) (A B : Finset (Fin d)) (f : MvPolynomial σ K) : relRank blk A B f ≤ √(↑(Fintype.card (MvPolynomial.BlockChoice blk A)) / ↑(Fintype.card (MvPolynomial.BlockChoice blk B)))

Imbalance ([LimayeSrinivasanTavenas2021, Claim 7(1), p. 6]): the relative rank is at most the square root of the number of rows divided by the number of columns. Together with relRank_le_sqrt_cols_div_rows it bounds the relative rank by the square root of the smaller dimension over the larger, 2 ^ (-|w_[d]| / 2) in the notation of the source, which is Claim 7(1).

theorem Cslib.Circuits.Arithmetic.relRank_le_sqrt_cols_div_rows {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] (blk : σ → Fin d) (A B : Finset (Fin d)) (f : MvPolynomial σ K) : relRank blk A B f ≤ √(↑(Fintype.card (MvPolynomial.BlockChoice blk B)) / ↑(Fintype.card (MvPolynomial.BlockChoice blk A)))

Imbalance ([LimayeSrinivasanTavenas2021, Claim 7(1), p. 6]): the relative rank is at most the square root of the number of columns divided by the number of rows; see relRank_le_sqrt_rows_div_cols for the other order.

theorem Cslib.Circuits.Arithmetic.relRank_le_one {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] (blk : σ → Fin d) (A B : Finset (Fin d)) (f : MvPolynomial σ K) : relRank blk A B f ≤ 1

The relative rank is at most 1, as noted in the display defining relrk_w in [LimayeSrinivasanTavenas2021, §2.1, p. 6].

theorem Cslib.Circuits.Arithmetic.rank_relMatrix_add_le {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] (blk : σ → Fin d) (A B : Finset (Fin d)) (f g : MvPolynomial σ K) : (relMatrix blk A B (f + g)).rank ≤ (relMatrix blk A B f).rank + (relMatrix blk A B g).rank

Subadditivity of rank for relative-rank matrices.

theorem Cslib.Circuits.Arithmetic.relRank_add_le {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] (blk : σ → Fin d) (A B : Finset (Fin d)) (f g : MvPolynomial σ K) : relRank blk A B (f + g) ≤ relRank blk A B f + relRank blk A B g

Subadditivity ([LimayeSrinivasanTavenas2021, Claim 7(2), p. 7]).

theorem Cslib.Circuits.Arithmetic.relRank_smul_le {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] (blk : σ → Fin d) (A B : Finset (Fin d)) (c : K) (f : MvPolynomial σ K) : relRank blk A B (c • f) ≤ relRank blk A B f

Scaling does not increase the relative rank.

theorem Cslib.Circuits.Arithmetic.relRank_smul {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] (blk : σ → Fin d) (A B : Finset (Fin d)) {c : K} (hc : c ≠ 0) (f : MvPolynomial σ K) : relRank blk A B (c • f) = relRank blk A B f

Scaling by a nonzero constant does not change the relative rank.

@[simp]

theorem Cslib.Circuits.Arithmetic.relRank_neg {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] (blk : σ → Fin d) (A B : Finset (Fin d)) (f : MvPolynomial σ K) : relRank blk A B (-f) = relRank blk A B f

Negation does not change the relative rank.

theorem Cslib.Circuits.Arithmetic.rank_relMatrix_mul_le {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] {blk : σ → Fin d} {A B S T : Finset (Fin d)} {f g : MvPolynomial σ K} (hf : MvPolynomial.IsSetMultilinear blk S f) (hg : MvPolynomial.IsSetMultilinear blk T g) (hST : Disjoint S T) (hA : A ⊆ S ∪ T) (hB : B ⊆ S ∪ T) : (relMatrix blk A B (f * g)).rank ≤ (relMatrix blk (A ∩ S) (B ∩ S) f).rank * (relMatrix blk (A ∩ T) (B ∩ T) g).rank

Rank multiplicativity, as an inequality: for set-multilinear factors on disjoint blocks, the rank of the product's matrix is at most the product of the ranks of the factors' matrices.

theorem Cslib.Circuits.Arithmetic.relRank_mul_le {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] {blk : σ → Fin d} {A B S T : Finset (Fin d)} {f g : MvPolynomial σ K} (hf : MvPolynomial.IsSetMultilinear blk S f) (hg : MvPolynomial.IsSetMultilinear blk T g) (hST : Disjoint S T) (hA : A ⊆ S ∪ T) (hB : B ⊆ S ∪ T) : relRank blk A B (f * g) ≤ relRank blk (A ∩ S) (B ∩ S) f * relRank blk (A ∩ T) (B ∩ T) g

Multiplicativity, as an inequality, binary case ([LimayeSrinivasanTavenas2021, Claim 7(3), p. 7]): if f and g are set-multilinear on disjoint sets S and T of blocks, which cover the row and column blocks, then the relative rank of f * g is at most the product of the relative ranks of f on the blocks of S and g on the blocks of T. LST state equality; their lower bound uses only this direction. See relRank_prod_le for finite products.

theorem Cslib.Circuits.Arithmetic.relRank_prod_le {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] {blk : σ → Fin d} {A B : Finset (Fin d)} {ι : Type u_3} (s : Finset ι) {f : ι → MvPolynomial σ K} {T : ι → Finset (Fin d)} (hT : (↑s).PairwiseDisjoint T) (hf : ∀ i ∈ s, MvPolynomial.IsSetMultilinear blk (T i) (f i)) (hA : A ⊆ s.biUnion T) (hB : B ⊆ s.biUnion T) : relRank blk A B (∏ i ∈ s, f i) ≤ ∏ i ∈ s, relRank blk (A ∩ T i) (B ∩ T i) (f i)

Multiplicativity, as an inequality ([LimayeSrinivasanTavenas2021, Claim 7(3), p. 7]): if the factors f i of a finite product are set-multilinear on pairwise disjoint sets T i of blocks, which together cover the row and column blocks, then the relative rank of the product is at most the product of the relative ranks of each f i on the blocks of T i. LST state equality for a partition of all the blocks; their lower bound uses only this direction.

theorem Cslib.Circuits.Arithmetic.relRank_rename {σ : Type u_1} {K : Type u_2} {d : ℕ} [Fintype σ] [Field K] {blk : σ → Fin d} {τ : Type u_3} [Fintype τ] {blk' : τ → Fin d} (e : σ ≃ τ) (he : ∀ (x : σ), blk' (e x) = blk x) (A B : Finset (Fin d)) (f : MvPolynomial σ K) : relRank blk' A B ((MvPolynomial.rename ⇑e) f) = relRank blk A B f

The relative rank is invariant under renaming the variables along their blocks (original).