theorem BooleanFourier.one_sub_pow_le_mul_card (t : ℝ) (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) (k : ℕ) : 1 - (1 - t) ^ k ≤ t * ↑k

theorem BooleanFourier.noiseSensitivity_le_delta_mul_totalInfluenceReal {n : ℕ} (δ : ℝ) (hδ₀ : 0 ≤ δ) (hδ₁ : δ ≤ 1 / 2) (f : (Fin n → Bool) → ℝ) : 1 / 2 * ∑ S : Finset (Fin n), (1 - (1 - 2 * δ) ^ S.card) * fourierCoeff f S ^ 2 ≤ δ * totalInfluenceReal f

theorem BooleanFourier.noiseSensitivity_le_delta_mul_totalInfluence {n : ℕ} (δ : ℝ) (hδ₀ : 0 ≤ δ) (hδ₁ : δ ≤ 1 / 2) (f : (Fin n → Bool) → Bool) : noiseSensitivity δ f ≤ δ * totalInfluenceReal fun (x : Fin n → Bool) => boolToReal (f x)