def BooleanFourier.IsMonotone {n : ℕ} (f : (Fin n → Bool) → Bool) : Prop

theorem BooleanFourier.Bool.false_true_of_le_ne {a b : Bool} (hle : a ≤ b) (hne : a ≠ b) : a = false ∧ b = true

theorem BooleanFourier.chi_singleton {n : ℕ} (i : Fin n) (x : Fin n → Bool) : chi {i} x = boolToReal (x i)

theorem BooleanFourier.flipCoord_flipCoord {n : ℕ} (x : Fin n → Bool) (i : Fin n) : flipCoord (flipCoord x i) i = x

theorem BooleanFourier.flipCoord_ne_self' {n : ℕ} (x : Fin n → Bool) (i : Fin n) : flipCoord x i ≠ x

theorem BooleanFourier.le_flipCoord_of_false {n : ℕ} (x : Fin n → Bool) (i : Fin n) (hxi : x i = false) : x ≤ flipCoord x i

theorem BooleanFourier.flipCoord_le_of_true {n : ℕ} (x : Fin n → Bool) (i : Fin n) (hxi : x i = true) : flipCoord x i ≤ x

theorem BooleanFourier.monotone_fourierCoeff_singleton_eq_influence {n : ℕ} (f : (Fin n → Bool) → Bool) (hf : Monotone f) (i : Fin n) : fourierCoeff (fun (x : Fin n → Bool) => boolToReal (f x)) {i} = influence f i