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

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

theorem BooleanFourier.threshold_width_log_ratio {n : ℕ} (f : (Fin n → Bool) → Bool) (hmon : IsMonotone f) (hI : totalInfluence f > 0) (ε : ℝ) (hε_pos : 0 < ε) (hε_lt : ε < 1 / 2) : thresholdValue f (1 - ε) - thresholdValue f ε ≤ Real.log ((1 - ε) / ε) / (2 * totalInfluence f)