Words

The words of Limaye, Srinivasan and Tavenas [LimayeSrinivasanTavenas2021, §2, p. 6]. A word is a tuple w : Fin d → ℤ. Its variables X(w) (WordVar w) form d blocks, block i having 2 ^ |w i| variables labelled by the bit strings of length |w i|, here the numbers below 2 ^ |w i|; a choice of one variable in every block (WordChoice w) is a set-multilinear monomial on all blocks. The blocks with 0 ≤ w i are positive (wordPos w, LST's P_w), the others negative (wordNeg w, LST's N_w). A word is b-unbiased (IsUnbiased w b) when every prefix sum has absolute value at most b.

The proof of LST Lemma 13 (§4, p. 10) builds an unbiased word greedily over an alphabet {a, -k}: the next letter is a when the sum of the letters so far is at most 0, and -k otherwise (greedyWord). It is k-unbiased when 0 ≤ a ≤ k (isUnbiased_greedyWord). The proof of LST Lemma 15 (§5, p. 12) uses this word with a = ⌊k / √2⌋.

Main definitions

• Cslib.Circuits.Arithmetic.WordVar, Cslib.Circuits.Arithmetic.WordChoice: the variables X(w) and the set-multilinear monomials on all blocks.
• Cslib.Circuits.Arithmetic.wordBlocks, Cslib.Circuits.Arithmetic.wordPos, Cslib.Circuits.Arithmetic.wordNeg: the positive and negative blocks.
• Cslib.Circuits.Arithmetic.IsUnbiased: b-unbiased words.
• Cslib.Circuits.Arithmetic.greedyWord: the greedy word of the proof of LST Lemma 13.

Main results

• Cslib.Circuits.Arithmetic.sum_filter_greedyWord: the prefix sums of the greedy word.
• Cslib.Circuits.Arithmetic.isUnbiased_greedyWord: the greedy word is k-unbiased.

References

• N. Limaye, S. Srinivasan, S. Tavenas, Superpolynomial lower bounds against low-depth algebraic circuits, ECCC TR21-081 revision 1, §2 (words, unbiasedness, p. 6) and the proof of Lemma 13 (§4, p. 10). The encoding of bit strings by numbers is original.

Variables and blocks

@[reducible, inline]

abbrev Cslib.Circuits.Arithmetic.WordVar {d : ℕ} (w : Fin d → ℤ) : Type

The variables X(w) of a word w: block i has 2 ^ |w i| variables, labelled by the numbers below 2 ^ |w i|, that is, by the bit strings of length |w i|.

@[reducible, inline]

abbrev Cslib.Circuits.Arithmetic.WordChoice {d : ℕ} (w : Fin d → ℤ) : Type

A choice of one variable in every block of X(w): a set-multilinear monomial.

def Cslib.Circuits.Arithmetic.wordBlocks {d : ℕ} (w : Fin d → ℤ) (p : ℤ → Prop) [DecidablePred p] : Finset (Fin d)

The blocks of w whose signed length satisfies p.

@[reducible, inline]

abbrev Cslib.Circuits.Arithmetic.wordPos {d : ℕ} (w : Fin d → ℤ) : Finset (Fin d)

The positive blocks P_w = {i | 0 ≤ w i} of a word.

@[reducible, inline]

abbrev Cslib.Circuits.Arithmetic.wordNeg {d : ℕ} (w : Fin d → ℤ) : Finset (Fin d)

The negative blocks N_w = {i | w i < 0} of a word.

@[simp]

theorem Cslib.Circuits.Arithmetic.mem_wordBlocks {d : ℕ} {w : Fin d → ℤ} {p : ℤ → Prop} [DecidablePred p] {i : Fin d} : i ∈ wordBlocks w p ↔ p (w i)

A block belongs to wordBlocks w p exactly when its signed length satisfies p.

theorem Cslib.Circuits.Arithmetic.compl_wordPos {d : ℕ} {w : Fin d → ℤ} : (wordPos w)ᶜ = wordNeg w

The negative blocks are the blocks that are not positive.

Unbiased words

def Cslib.Circuits.Arithmetic.IsUnbiased {d : ℕ} (w : Fin d → ℤ) (b : ℕ) : Prop

A word is b-unbiased when every prefix sum ∑ i < t, w i has absolute value at most b (LST §2, p. 6).

The greedy word (LST, proof of Lemma 13)

def Cslib.Circuits.Arithmetic.greedyPrefix (a k : ℤ) : ℕ → ℤ

The prefix sums of the greedy word over the alphabet {a, -k}: start at 0, then add a when the current sum is at most 0, and add -k otherwise.

def Cslib.Circuits.Arithmetic.greedyWord (a k : ℤ) (d : ℕ) (i : Fin d) : ℤ

The greedy word of length d over the alphabet {a, -k} (LST, proof of Lemma 13, p. 10; used with a = ⌊k / √2⌋ in the proof of Lemma 15, p. 12): its i-th letter is a if the sum of the earlier letters is at most 0, and -k otherwise.

theorem Cslib.Circuits.Arithmetic.greedyWord_eq_or {d : ℕ} (a k : ℤ) (i : Fin d) : greedyWord a k d i = a ∨ greedyWord a k d i = -k

Every letter of the greedy word is a or -k.

theorem Cslib.Circuits.Arithmetic.sum_filter_greedyWord {d : ℕ} (a k : ℤ) {t : ℕ} (ht : t ≤ d) : ∑ i : Fin d with ↑i < t, greedyWord a k d i = greedyPrefix a k t

The prefix sums of the greedy word are the values of greedyPrefix.

theorem Cslib.Circuits.Arithmetic.greedyPrefix_mem_Icc {a k : ℤ} (ha : 0 ≤ a) (hk : 0 ≤ k) (t : ℕ) : -k ≤ greedyPrefix a k t ∧ greedyPrefix a k t ≤ a

The prefix sums of the greedy word stay in [-k, a] when 0 ≤ a and 0 ≤ k.

theorem Cslib.Circuits.Arithmetic.isUnbiased_greedyWord {d : ℕ} {a : ℤ} {k : ℕ} (ha : 0 ≤ a) (hak : a ≤ ↑k) : IsUnbiased (greedyWord a (↑k) d) k

The greedy word is k-unbiased (LST, proof of Lemma 13): if 0 ≤ a ≤ k, every prefix sum of the greedy word over {a, -k} has absolute value at most k.