noncomputable def BooleanFourier.majorityFn (n : ℕ) : (Fin n → Bool) → ℝ

theorem BooleanFourier.majorityFn_compl {n : ℕ} (hn : Odd n) (x : Fin n → Bool) : (majorityFn n fun (i : Fin n) => !x i) = -majorityFn n x

theorem BooleanFourier.chi_compl {n : ℕ} (S : Finset (Fin n)) (x : Fin n → Bool) : (chi S fun (i : Fin n) => !x i) = (-1) ^ S.card * chi S x

theorem BooleanFourier.fourierCoeff_majorityFn_even_eq_zero {n : ℕ} (hn : Odd n) (S : Finset (Fin n)) (hS : Even S.card) : fourierCoeff (majorityFn n) S = 0

noncomputable def BooleanFourier.signFn : ℝ → ℝ

noncomputable def BooleanFourier.gaussianSignCorrelation (ρ : ℝ) : ℝ

theorem BooleanFourier.sheppard_formula_local (ρ : ℝ) (hρ_gt : -1 < ρ) (hρ_lt : ρ < 1) : gaussianSignCorrelation ρ = 2 / Real.pi * Real.arcsin ρ

theorem BooleanFourier.majority_noiseStability_tendsto_gaussian (ρ : ℝ) (hρ_gt : -1 < ρ) (hρ_lt : ρ < 1) : Filter.Tendsto (fun (k : ℕ) => noiseStability ρ (majorityFn (2 * k + 1))) Filter.atTop (nhds (gaussianSignCorrelation ρ))

theorem BooleanFourier.noiseStability_majority_tendsto (ρ : ℝ) (hρ_gt : -1 < ρ) (hρ_lt : ρ < 1) : Filter.Tendsto (fun (k : ℕ) => noiseStability ρ (majorityFn (2 * k + 1))) Filter.atTop (nhds (2 / Real.pi * Real.arcsin ρ))