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

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

theorem BooleanFourier.margulis_sharp_threshold : ∃ C > 0, ∀ (n : ℕ) (f : (Fin n → Bool) → Bool), vertexBoundaryMeasure f * totalInfluence f ≥ C * boolVariance f ^ 2