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

theorem BooleanFourier.influence_nonneg {n : ℕ} (f : (Fin n → Bool) → Bool) (i : Fin n) : 0 ≤ influence f i

theorem BooleanFourier.high_influence_count_le {n : ℕ} (f : (Fin n → Bool) → Bool) (τ : ℝ) (hτ : 0 < τ) : ↑(highInfluenceCoords f τ).card ≤ totalInfluence f / τ