OAI.LeanBlast.GotsmanLinial.gotsmanLinialStatement

The theorem states the Gotsman-Linial bound, defined as the proposition GotsmanLinialStatement, with no extra hypotheses. Vertices of the cube are functions from Fin n to Bool, read as points of {-1,1}^n with true as 1 and false as -1. For natural numbers n and d with 1 ≤ n, 1 ≤ d and d ≤ n, take any real multilinear polynomial p in n variables, meaning every monomial in its support has exponent at most 1 in each variable, and assume its total degree is at most d. Evaluate p at a cube vertex and apply the sign threshold that returns 1 when the value is nonnegative and -1 otherwise. The claim is that the average sensitivity of this threshold function is at most 8·d·√n. Average sensitivity is the sum over coordinates i of the number of vertices x whose value changes when coordinate i is flipped, each count divided by 2^n. The statement is admitted without proof.