theorem BooleanFourier.friedgut_level_concentration {n : ℕ} (f : (Fin n → Bool) → Bool) (ε : ℝ) (hε : 0 < ε) (hVar : varianceReal (liftPM f) > 0) : ∃ (J : Finset (Fin n)), ↑J.card ≤ 2 ^ (4 * totalInfluence f / (ε * varianceReal (liftPM f))) ∧ ∑ S : Finset (Fin n) with ¬S ⊆ J, fourierCoeff (liftPM f) S ^ 2 ≤ ε ^ 2 / 4

theorem BooleanFourier.friedgut_junta_theorem_2_1 : ∃ C > 0, ∀ (n : ℕ) (f : (Fin n → Bool) → Bool) (ε : ℝ), varianceReal (liftPM f) > 0 → ε > 0 → ∃ (g : (Fin n → Bool) → Bool) (J : ℕ), IsBoolFnJunta g J ∧ ↑J ≤ 2 ^ (C * totalInfluence f / (ε * varianceReal (liftPM f))) ∧ boolL2Dist f g ≤ ε

theorem BooleanFourier.friedgut_junta_corollary_bound {n : ℕ} (f : (Fin n → Bool) → Bool) (K : ℝ) (hVar : varianceReal (liftPM f) > 0) (hK1 : K ≥ 1) (hIK : totalInfluence f ≤ K * varianceReal (liftPM f)) : ∃ (i : Fin n), influence f i ≥ Real.exp (-5 * K)

theorem BooleanFourier.friedgut_junta_theorem : ∃ C > 0, ∀ (n : ℕ) (f : (Fin n → Bool) → Bool) (K : ℝ), varianceReal (liftPM f) > 0 → K ≥ 1 → totalInfluence f ≤ K * varianceReal (liftPM f) → ∃ (i : Fin n), influence f i ≥ Real.exp (-C * K)