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

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

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

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

theorem BooleanFourier.fkn_theorem {n : ℕ} (hn : 0 < n) (f : (Fin n → Bool) → Bool) (ε : ℝ) (hε : 0 ≤ ε) (hW : (fourierWeightAbove 1 fun (x : Fin n → Bool) => boolToReal (f x)) ≤ ε) : ∃ (i : Fin n), boolDist f (dictator i) ≤ ε ∨ boolDist f (negDictator i) ≤ ε