noncomputable def GaussianStability.signFn : ℝ → ℝ

noncomputable def GaussianStability.gaussianNoiseStabilitySign (ρ : ℝ) : ℝ

theorem GaussianStability.sheppard_formula (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) : gaussianNoiseStabilitySign ρ = 2 / Real.pi * Real.arcsin ρ

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