def BooleanFourier.boolToSign (b : Bool) : ℝ

noncomputable def BooleanFourier.boolDiscreteDerivative {n : ℕ} (g : (Fin (n + 1) → Bool) → ℝ) (i : Fin (n + 1)) : (Fin n → Bool) → ℝ

@[simp]

theorem BooleanFourier.boolDiscreteDerivative_apply {n : ℕ} (g : (Fin (n + 1) → Bool) → ℝ) (i : Fin (n + 1)) (y : Fin n → Bool) : boolDiscreteDerivative g i y = 1 / 2 * (g (i.insertNth true y) - g (i.insertNth false y))

theorem BooleanFourier.flipCoord_insertNth {n : ℕ} (i : Fin (n + 1)) (b : Bool) (y : Fin n → Bool) : flipCoord (i.insertNth b y) i = i.insertNth (!b) y

theorem BooleanFourier.ne_flipCoord_iff_insertNth {n : ℕ} (f : (Fin (n + 1) → Bool) → Bool) (i : Fin (n + 1)) (b : Bool) (y : Fin n → Bool) : f (i.insertNth b y) ≠ f (flipCoord (i.insertNth b y) i) ↔ f (i.insertNth true y) ≠ f (i.insertNth false y)

theorem BooleanFourier.influence_filter_card_eq {n : ℕ} (f : (Fin (n + 1) → Bool) → Bool) (i : Fin (n + 1)) : {x : Fin (n + 1) → Bool | f x ≠ f (flipCoord x i)}.card = 2 * {y : Fin n → Bool | f (i.insertNth true y) ≠ f (i.insertNth false y)}.card

theorem BooleanFourier.influence_eq_l2_norm_sq_discreteDerivative {n : ℕ} (f : (Fin (n + 1) → Bool) → Bool) (i : Fin (n + 1)) : influence f i = (∑ y : Fin n → Bool, boolDiscreteDerivative (fun (x : Fin (n + 1) → Bool) => boolToSign (f x)) i y ^ 2) / 2 ^ n