Gotsman--Linial: Statement

Adapted from OpenAI's formalization of Average Sensitivity of Polynomial Threshold Functions (25 September 2026), at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/GotsmanLinial/Statement.lean

The original Boolean-cube representation is used internally in this proof development; Complexitylib.BooleanAnalysis.PolynomialThreshold transports the result to the library's Fourier and influence API. Changes here adapt module visibility, namespace names, formatting, and redundant simp attributes to complexitylib.

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flip_apply_same {n : ℕ} (i : Fin n) (x : Cube n) : flip i x i = !x i

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flip_apply_ne {n : ℕ} (i : Fin n) (x : Cube n) (j : Fin n) (h : j ≠ i) : flip i x j = x j

@[simp]

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

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flip_ne_self {n : ℕ} (i : Fin n) (x : Cube n) : flip i x ≠ x

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flip_injective_direction {n : ℕ} (x : Cube n) : Function.Injective fun (i : Fin n) => flip i x

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flip_involutive {n : ℕ} (i : Fin n) : Function.Involutive (flip i)

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.flip_bijective {n : ℕ} (i : Fin n) : Function.Bijective (flip i)

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.cubeCoord_flip_same {n : ℕ} (x : Cube n) (i : Fin n) : cubeCoord (flip i x) i = -cubeCoord x i

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.cubeCoord_flip_ne {n : ℕ} (x : Cube n) (i j : Fin n) (h : j ≠ i) : cubeCoord (flip i x) j = cubeCoord x j

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.cubeCoord_cases {n : ℕ} (x : Cube n) (i : Fin n) : cubeCoord x i = 1 ∨ cubeCoord x i = -1

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.cubeCoord_sq {n : ℕ} (x : Cube n) (i : Fin n) : cubeCoord x i ^ 2 = 1

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.thresholdSign_zero : thresholdSign 0 = 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.thresholdSign_eq_one_iff (t : ℝ) : thresholdSign t = 1 ↔ 0 ≤ t

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.thresholdSign_eq_neg_one_iff (t : ℝ) : thresholdSign t = -1 ↔ t < 0

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.thresholdSign_cases (t : ℝ) : thresholdSign t = 1 ∨ thresholdSign t = -1

@[simp]

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.thresholdSign_sq (t : ℝ) : thresholdSign t ^ 2 = 1

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.card_cube (n : ℕ) : Fintype.card (Cube n) = 2 ^ n

noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.cubeEquivSignVectors (n : ℕ) : Cube n ≃ { x : Fin n → ℝ // ∀ (i : Fin n), x i = 1 ∨ x i = -1 }

The Boolean encoding represents every sign vector exactly once.

Equations

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

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.averageSensitivity_eq_count {n : ℕ} (f : Cube n → ℝ) : averageSensitivity f = ↑(sensitiveEdgeCount f) / 2 ^ n

theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.averageSensitivity_eq_uniform {n : ℕ} (f : Cube n → ℝ) : averageSensitivity f = ∑ i : Fin n, ↑(sensitiveVertices f i).card / ↑(Fintype.card (Cube n))