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

theorem BooleanFourier.monotone_update_le {n : ℕ} (f : (Fin n → Bool) → Bool) (hf : IsMonotone f) (i : Fin n) (x : Fin n → Bool) : f (Function.update x i false) ≤ f (Function.update x i true)

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

theorem BooleanFourier.monotone_pair_sum {n : ℕ} (f : (Fin n → Bool) → Bool) (hf : IsMonotone f) (i : Fin n) (x : Fin n → Bool) : boolToReal (f x) * boolToReal (x i) + boolToReal (f (flipCoord x i)) * boolToReal (flipCoord x i i) = if f x ≠ f (flipCoord x i) then 2 else 0

theorem BooleanFourier.sum_boolToReal_eq_card_of_monotone {n : ℕ} (f : (Fin n → Bool) → Bool) (hf : IsMonotone f) (i : Fin n) : ∑ x : Fin n → Bool, boolToReal (f x) * boolToReal (x i) = ↑{x : Fin n → Bool | f x ≠ f (flipCoord x i)}.card

theorem BooleanFourier.fourierCoeff_singleton_eq_influence_of_monotone {n : ℕ} (f : (Fin n → Bool) → Bool) (hf : IsMonotone f) (i : Fin n) : fourierCoeff (liftPM f) {i} = influence f i