def BooleanFourier.flipCoord {n : ℕ} (x : Fin n → Bool) (i : Fin n) : Fin n → Bool

noncomputable def BooleanFourier.influence {n : ℕ} (f : (Fin n → Bool) → Bool) (i : Fin n) : ℝ

noncomputable def BooleanFourier.totalInfluence {n : ℕ} (f : (Fin n → Bool) → Bool) : ℝ

def BooleanFourier.numPivotal {n : ℕ} (f : (Fin n → Bool) → Bool) (x : Fin n → Bool) : ℕ

theorem BooleanFourier.totalInfluence_eq_expected_pivotal {n : ℕ} (f : (Fin n → Bool) → Bool) : totalInfluence f = 1 / 2 ^ n * ∑ x : Fin n → Bool, ↑(numPivotal f x)