Documentation

Complexity.Foundations.BooleanAnalysis.PolynomialCorrelation

Exponential correlation bounds for polynomials over ๐”ฝโ‚‚ #

For odd โ„“, the exclusive or of the majorities of k disjoint blocks of โ„“ bits (BitString.xorMajority) has correlation at most (2 d / โˆšโ„“) ^ k with every Boolean function of degree at most d over ๐”ฝโ‚‚ = ZMod 2 (BitString.abs_expect_signVal_xorMajority_mul_signVal_le) Chattopadhyay et al., Theorem 1.1.

Write โ„“ = 2 m + 1; the proof counts dimensions Chattopadhyay et al., Section 2. Every function on a block is q + Maj ยท r with q and r of degree at most m (BitString.exists_eq_add_majority_mul), so the products over the blocks of a monomial of at most m bits of the block, possibly times the majority of the block, span all functions on the k blocks. Weigh a block by the size of its monomial, or by m + 1 when it carries its majority, and a product by the sum of the weights of its blocks: multiplying by a function of degree d raises the weight by at most d Chattopadhyay et al., Lemma 2.2. Where a function P of degree d agrees with the exclusive or of the majorities, the majority of a block is P plus the other majorities. So if the first block whose monomial has at most m - d bits carries its majority, the product agrees there with a combination of products of smaller weight and of products in which that block does not carry its majority. By induction on the weight, the latter products span all functions on the inputs where P agrees with the exclusive or of the majorities Chattopadhyay et al., Lemma 2.3, and there are about half as many of them as there are inputs. Hence P agrees with the exclusive or of the majorities on at most (2 ^ (k โ„“) + (2 N) ^ k) / 2 inputs, where N counts the sets A of bits of a block with m - d < |A| โ‰ค m (BitString.two_mul_card_agree_xorMajority_le). This bounds the correlation by (2 N / 2 ^ โ„“) ^ k (BitString.abs_expect_signVal_xorMajority_mul_signVal_le_card), and N โ‰ค d C(โ„“, m) โ‰ค d 2 ^ โ„“ / โˆšโ„“.

Main definitions #

Main results #

References #

source
def Cslib.BitString.xorMajority (k โ„“ : โ„•) :
BooleanFunction (k * โ„“)

The exclusive or of the majorities of the k blocks block x i of โ„“ consecutive bits of a string x of k * โ„“ bits.

Instances For

    Interpolation and the majority decomposition #

    source
    theorem Cslib.BitString.exists_mem_lowDegree_forall_weight_le_eq {R : Type u_1} [CommRing R] {n : โ„•} (D : โ„•) (f : BitString n โ†’ R) :
    โˆƒ q โˆˆ lowDegree R (Fin n) D, โˆ€ (x : Fin n โ†’ Bool), weight x โ‰ค D โ†’ q x = f x

    Interpolation on a Hamming ball: every function agrees on the strings of weight at most D with a function of degree at most D.

    source
    theorem Cslib.BitString.exists_eq_add_majority_mul {R : Type u_1} [CommRing R] {m : โ„•} (f : BitString (2 * m + 1) โ†’ R) :
    โˆƒ q โˆˆ lowDegree R (Fin (2 * m + 1)) m, โˆƒ r โˆˆ lowDegree R (Fin (2 * m + 1)) m, โˆ€ (x : BitString (2 * m + 1)), f x = q x + bitVal R (majority (2 * m + 1) x) * r x

    The majority decomposition: every function on 2 m + 1 bits is q + Maj ยท r, with the majority read as 0 or 1 in R and q and r of degree at most m. The function q interpolates on the strings of weight at most m, where the majority is false, and r on the others, which are the negations of the former Chattopadhyay et al., Section 2.1.

    Counting the tuples whose first good flag is unset #

    Products of monomials and majorities of blocks #

    Counting dimensions #

    source
    theorem Cslib.BitString.two_mul_card_agree_xorMajority_le {k m d : โ„•} {P : BitString (k * (2 * m + 1)) โ†’ ZMod 2} (hP : P โˆˆ lowDegree (ZMod 2) (Fin (k * (2 * m + 1))) d) :
    2 * {x : BitString (k * (2 * m + 1)) | P x = bitVal (ZMod 2) (xorMajority k (2 * m + 1) x)}.card โ‰ค 2 ^ (k * (2 * m + 1)) + (2 * {A : Finset (Fin (2 * m + 1)) | A.card โ‰ค m โˆง m < A.card + d}.card) ^ k

    A function of low degree agrees with the exclusive or of majorities on few inputs: if P has degree at most d over ZMod 2 on k blocks of 2 m + 1 bits, twice the number of inputs on which P agrees with the exclusive or of the majorities of the blocks is at most 2 ^ (k (2 m + 1)) + (2 N) ^ k, where N is the number of sets A of bits of a block with m - d < |A| โ‰ค m Chattopadhyay et al., Section 2.3.

    Correlation #

    source
    theorem Cslib.BitString.abs_expect_signVal_xorMajority_mul_signVal_le_card {k m d : โ„•} {p : BooleanFunction (k * (2 * m + 1))} (hp : (fun (x : BitString (k * (2 * m + 1))) => bitVal (ZMod 2) (p x)) โˆˆ lowDegree (ZMod 2) (Fin (k * (2 * m + 1))) d) :
    |Finset.univ.expect fun (x : BitString (k * (2 * m + 1))) => signVal (xorMajority k (2 * m + 1) x) * signVal (p x)| โ‰ค (2 * โ†‘{A : Finset (Fin (2 * m + 1)) | A.card โ‰ค m โˆง m < A.card + d}.card / 2 ^ (2 * m + 1)) ^ k

    The correlation bound by the middle band: for a Boolean function p of degree at most d over ZMod 2 on k blocks of 2 m + 1 bits, the correlation of the exclusive or of the majorities of the blocks with p, read as signs, is at most (2 N / 2 ^ (2 m + 1)) ^ k in absolute value, where N is the number of sets A of bits of a block with m - d < |A| โ‰ค m Chattopadhyay et al., Section 2.3.

    source
    theorem Cslib.BitString.abs_expect_signVal_xorMajority_mul_signVal_le {k โ„“ d : โ„•} (hโ„“ : Odd โ„“) {p : BooleanFunction (k * โ„“)} (hp : (fun (x : BitString (k * โ„“)) => bitVal (ZMod 2) (p x)) โˆˆ lowDegree (ZMod 2) (Fin (k * โ„“)) d) :
    |Finset.univ.expect fun (x : BitString (k * โ„“)) => signVal (xorMajority k โ„“ x) * signVal (p x)| โ‰ค (2 * โ†‘d / โˆšโ†‘โ„“) ^ k

    Exponential correlation bound for polynomials: for odd โ„“, the correlation of the exclusive or of the majorities of k disjoint blocks of โ„“ bits with a Boolean function p of degree at most d over ZMod 2, read as signs, is at most (2 d / โˆšโ„“) ^ k in absolute value Chattopadhyay et al., Theorem 1.1.