Transport of the average-sensitivity bound

The source proof uses Boolean coordinates with true representing +1. The equivalence below respects coordinate flips and uniform expectation, so its average sensitivity agrees with the canonical Fourier total influence.

def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.cubeEquiv (n : ℕ) : Cube n ≃ BooleanAnalysis.Cube n

Translate the source's sign encoding to the library's additive binary cube.

Equations

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

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.cubeEquiv_flip {n : ℕ} (i : Fin n) (x : Cube n) : (cubeEquiv n) (flip i x) = flipCoord i ((cubeEquiv n) x)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.cubeEquiv_chi {n : ℕ} (x : Cube n) : (fun (i : Fin n) => chi ((cubeEquiv n) x i)) = cubeCoord x

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomialThreshold_cubeEquiv {n : ℕ} (p : MvPolynomial (Fin n) ℝ) (x : Cube n) : BooleanAnalysis.polynomialThreshold p ((cubeEquiv n) x) = polynomialThreshold p x

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.totalInfluence_eq_averageSensitivity {n : ℕ} (f : BooleanFunction n) (hf : IsBooleanValued f) : totalInfluence f = averageSensitivity fun (x : Cube n) => f ((cubeEquiv n) x)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.polynomialThreshold_isBooleanValued {n : ℕ} (p : MvPolynomial (Fin n) ℝ) : IsBooleanValued (BooleanAnalysis.polynomialThreshold p)

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