The finite exponential correlation bound

Applying the agreement estimate to p and p + 1 bounds both signs of the correlation. The error is the kth power of a single-block middle-band fraction.

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.correlation_eq_card {α : Type u_1} [Fintype α] (f g : α → ZMod 2) : correlation f g = |(2 * ↑(Nat.card { x : α // f x = g x }) - ↑(Nat.card α)) / ↑(Nat.card α)|

theorem Complexity.BooleanAnalysis.PolynomialCorrelation.Internal.add_one_eq_iff (a b : ZMod 2) : a + 1 = b ↔ a ≠ b

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