noncomputable def BooleanFourier.disagreementProb {n : ℕ} (ρ : ℝ) (f : (Fin n → Bool) → ℝ) : ℝ

theorem BooleanFourier.disagreementProb_eq {n : ℕ} (ρ : ℝ) (f : (Fin n → Bool) → ℝ) : disagreementProb ρ f = (1 - noiseStability ρ f) / 2

noncomputable def BooleanFourier.noiseSensitivityReal {n : ℕ} (δ : ℝ) (f : (Fin n → Bool) → ℝ) : ℝ

theorem BooleanFourier.noiseSensitivityReal_eq {n : ℕ} (δ : ℝ) (f : (Fin n → Bool) → ℝ) : noiseSensitivityReal δ f = (1 - noiseStability (1 - 2 * δ) f) / 2

theorem BooleanFourier.noiseSensitivity_eq {n : ℕ} (δ : ℝ) (f : (Fin n → Bool) → Bool) : noiseSensitivity δ f = (1 - noiseStability (1 - 2 * δ) fun (x : Fin n → Bool) => boolToReal (f x)) / 2