theorem BooleanFourier.noiseStability_ge_fourierCoeff_empty_sq {n : ℕ} (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (f : (Fin n → Bool) → ℝ) : noiseStability ρ f ≥ fourierCoeff f ∅ ^ 2

theorem BooleanFourier.noiseStability_le_sum_sq {n : ℕ} (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) (f : (Fin n → Bool) → ℝ) : noiseStability ρ f ≤ ∑ S : Finset (Fin n), fourierCoeff f S ^ 2

theorem BooleanFourier.noiseStability_bounds {n : ℕ} (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) (f : (Fin n → Bool) → ℝ) : fourierCoeff f ∅ ^ 2 ≤ noiseStability ρ f ∧ noiseStability ρ f ≤ ∑ S : Finset (Fin n), fourierCoeff f S ^ 2

theorem BooleanFourier.noiseStability_le_one_of_boolean {n : ℕ} (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) (f : (Fin n → Bool) → Bool) : (noiseStability ρ fun (x : Fin n → Bool) => boolToReal (f x)) ≤ 1

theorem BooleanFourier.noiseStability_bounds_boolean {n : ℕ} (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) (f : (Fin n → Bool) → Bool) : (fourierCoeff (fun (x : Fin n → Bool) => boolToReal (f x)) ∅ ^ 2 ≤ noiseStability ρ fun (x : Fin n → Bool) => boolToReal (f x)) ∧ (noiseStability ρ fun (x : Fin n → Bool) => boolToReal (f x)) ≤ 1