theorem BooleanFourier.noiseStability_eq_fourier_sum {n : ℕ} (ρ : ℝ) (f : (Fin n → Bool) → ℝ) : noiseStability ρ f = ∑ S : Finset (Fin n), ρ ^ S.card * fourierCoeff f S ^ 2

theorem BooleanFourier.noiseStability_one {n : ℕ} (f : (Fin n → Bool) → ℝ) : noiseStability 1 f = ∑ S : Finset (Fin n), fourierCoeff f S ^ 2

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

theorem BooleanFourier.fourierCoeff_noiseOperator {n : ℕ} (ρ : ℝ) (f : (Fin n → Bool) → ℝ) (S : Finset (Fin n)) : fourierCoeff (noiseOperator ρ f) S = ρ ^ S.card * fourierCoeff f S