theorem BooleanFourier.noiseStability_mono {n : ℕ} (ρ σ : ℝ) (hρ₀ : 0 ≤ ρ) (hρσ : ρ ≤ σ) (f : (Fin n → Bool) → ℝ) : noiseStability ρ f ≤ noiseStability σ f

theorem BooleanFourier.noiseStability_at_zero {n : ℕ} (f : (Fin n → Bool) → ℝ) : noiseStability 0 f = fourierCoeff f ∅ ^ 2

theorem BooleanFourier.noiseStability_at_one_of_boolean {n : ℕ} (f : (Fin n → Bool) → Bool) : (noiseStability 1 fun (x : Fin n → Bool) => boolToReal (f x)) = 1

theorem BooleanFourier.noiseStability_bounds_of_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