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

theorem BooleanFourier.totalInfluence_le_n {n : ℕ} (f : (Fin n → Bool) → Bool) : totalInfluence f ≤ ↑n

def BooleanFourier.IsIntersectingFamily {n : ℕ} (F : Finset (Finset (Fin n))) : Prop

def BooleanFourier.IsJunta {n : ℕ} (F : Finset (Finset (Fin n))) (J : ℕ) : Prop

noncomputable def BooleanFourier.muPWeight (n : ℕ) (p : ℝ) (A : Finset (Fin n)) : ℝ

noncomputable def BooleanFourier.muPMeasure {n : ℕ} (F : Finset (Finset (Fin n))) (p : ℝ) : ℝ

def BooleanFourier.IsEpsCloseToIntersectingJunta {n : ℕ} (F : Finset (Finset (Fin n))) (p ε : ℝ) (J : ℕ) : Prop

theorem BooleanFourier.dinur_friedgut (ζ ε : ℝ) (hζ : ζ > 0) (hε : ε > 0) : ∃ (J : ℕ), ∀ (n : ℕ) (F : Finset (Finset (Fin n))) (p : ℝ), IsIntersectingFamily F → ζ < p → p < 1 - ζ → IsEpsCloseToIntersectingJunta F p ε J