Binary assignments and the public correlation bounds

The set-of-true-coordinates representation is equivalent to the ordinary binary cube. Correlation is unchanged by this bijection.

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.correlation_comm {α : Type u_1} [Fintype α] (f g : α → ZMod 2) : correlation f g = correlation g f

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.correlation_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (e : α ≃ β) (f g : β → ZMod 2) : (correlation (fun (x : α) => f (e x)) fun (x : α) => g (e x)) = correlation f g

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.bitsToBlocks_blockBits {k m : ℕ} (x : BlockCube k m) : bitsToBlocks (blockBits x) = x

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.blockBits_bitsToBlocks {k m : ℕ} (x : Fin k × Fin (2 * m + 1) → ZMod 2) : blockBits (bitsToBlocks x) = x

def Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.blockBitsEquiv {k m : ℕ} : BlockCube k m ≃ (Fin k × Fin (2 * m + 1) → ZMod 2)

The two Boolean input representations are in bijection.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.exceptional_card_eq (m d : ℕ) : Nat.card (ExceptionalAtom m d) = 2 * middleBandCount m d

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.correlation_middleBand_bound {k m d : ℕ} (p : MvPolynomial (Fin k × Fin (2 * m + 1)) (ZMod 2)) (hp : p.totalDegree ≤ d) : correlation xorMajority (polynomialEval p) ≤ (2 * ↑(middleBandCount m d) / 2 ^ (2 * m + 1)) ^ k

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.correlation_sqrt_bound {k m d : ℕ} (p : MvPolynomial (Fin k × Fin (2 * m + 1)) (ZMod 2)) (hp : p.totalDegree ≤ d) : correlation xorMajority (polynomialEval p) ≤ (2 * ↑d / √(2 * ↑m + 1)) ^ k

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.correlation_bits_bound {k m d : ℕ} (p : MvPolynomial (Fin k × Fin (2 * m + 1)) (ZMod 2)) (hp : p.totalDegree ≤ d) : (correlation xorMajorityBits fun (x : Fin k × Fin (2 * m + 1) → ZMod 2) => (MvPolynomial.eval x) p) ≤ (2 * ↑d / √(2 * ↑m + 1)) ^ k