def GaussianStability.IsPlusMinusOneValued {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) : Prop

noncomputable def GaussianStability.gaussianNoiseStabilityPM {n : ℕ} (ρ : ℝ) (f : EuclideanSpace ℝ (Fin n) → ℝ) : ℝ

def GaussianStability.IsHalfspaceThreshold {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) : Prop

noncomputable def GaussianStability.gaussianMean {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) : ℝ

theorem GaussianStability.gaussian_noise_stability_maximized_by_halfspace {n : ℕ} (ρ : ℝ) (hρ : ρ ∈ Set.Icc 0 1) (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf_pm : IsPlusMinusOneValued f) (g : EuclideanSpace ℝ (Fin n) → ℝ) (hg : IsHalfspaceThreshold g) (hfg_mean : gaussianMean f = gaussianMean g) : gaussianNoiseStabilityPM ρ f ≤ gaussianNoiseStabilityPM ρ g