theorem BooleanFourier.bourgain_noise_sensitivity : ∃ c > 0, ∀ (n : ℕ) (δ τ : ℝ) (f : (Fin n → Bool) → Bool), 0 < δ → δ ≤ 1 / 2 → 0 < τ → τ < 1 → (∀ (i : Fin n), fourierInfluence (fun (x : Fin n → Bool) => boolToReal (f x)) i ≤ τ) → noiseSensitivity δ f ≥ (c * variance fun (x : Fin n → Bool) => boolToReal (f x)) * min (δ * Real.log (1 / τ)) 1