Multilinear normal form on the sign cube

Reducing exponents modulo two preserves evaluation at signs, produces a multilinear polynomial, and never increases total degree. This removes the multilinearity hypothesis from the imported Gotsman--Linial theorem.

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMultilinearize_isMultilinear {n : ℕ} (p : MvPolynomial (Fin n) ℝ) : IsMultilinear (signMultilinearize p)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMultilinearize_totalDegree_le {n : ℕ} (p : MvPolynomial (Fin n) ℝ) : (signMultilinearize p).totalDegree ≤ p.totalDegree

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.signMultilinearize_eval {n : ℕ} (p : MvPolynomial (Fin n) ℝ) (x : Fin n → ℝ) (hx : ∀ (i : Fin n), x i ^ 2 = 1) : (MvPolynomial.eval x) (signMultilinearize p) = (MvPolynomial.eval x) p

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomialThreshold_signMultilinearize {n : ℕ} (p : MvPolynomial (Fin n) ℝ) : BooleanAnalysis.polynomialThreshold (signMultilinearize p) = BooleanAnalysis.polynomialThreshold p

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.totalInfluence_polynomialThreshold_le {n d : ℕ} (p : MvPolynomial (Fin n) ℝ) (hd : p.totalDegree ≤ d) : totalInfluence (BooleanAnalysis.polynomialThreshold p) ≤ 8 * ↑d * √↑n