theorem BooleanFourier.expect_sq_eq_one {n : ℕ} (f : BoolFn n) (hf : ∀ (x : Fin n → Bool), f x = 1 ∨ f x = -1) : (expect fun (x : Fin n → Bool) => f x ^ 2) = 1

theorem BooleanFourier.fourierInfluence_nonneg {n : ℕ} (f : BoolFn n) (i : Fin n) : fourierInfluence f i ≥ 0

theorem BooleanFourier.variance_le_one {n : ℕ} (f : BoolFn n) (hf : ∀ (x : Fin n → Bool), f x = 1 ∨ f x = -1) : variance f ≤ 1

theorem BooleanFourier.log_le_two_mul_sqrt {n : ℝ} (hn : 0 < n) : Real.log n ≤ 2 * √n

theorem BooleanFourier.kkl_theorem : ∃ c > 0, ∀ n ≥ 2, ∀ (f : BoolFn n), (∀ (x : Fin n → Bool), f x = 1 ∨ f x = -1) → ∃ (i : Fin n), fourierInfluence f i ≥ c * variance f * Real.log ↑n / ↑n

theorem BooleanFourier.variance_balanced_eq_one {n : ℕ} (f : BoolFn n) (hf : ∀ (x : Fin n → Bool), f x = 1 ∨ f x = -1) (hbal : expect f = 0) : variance f = 1

theorem BooleanFourier.kkl_balanced : ∃ c > 0, ∀ n ≥ 2, ∀ (f : BoolFn n), (∀ (x : Fin n → Bool), f x = 1 ∨ f x = -1) → expect f = 0 → ∃ (i : Fin n), fourierInfluence f i ≥ c * Real.log ↑n / ↑n