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

def BooleanFourier.IsBalanced {n : ℕ} (f : (Fin n → Bool) → ℝ) : Prop

def BooleanFourier.IsBooleanValued {n : ℕ} (f : (Fin n → Bool) → ℝ) : Prop

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

noncomputable def BooleanFourier.gaussianCDF (t : ℝ) : ℝ

noncomputable def BooleanFourier.gaussianCDFInv (p : ℝ) : ℝ

noncomputable def BooleanFourier.halfspaceNoiseStability01 (ρ μ : ℝ) : ℝ

noncomputable def BooleanFourier.halfspaceNoiseStability (ρ μ : ℝ) : ℝ

def BooleanFourier.HasBoundedRange01 {n : ℕ} (f : (Fin n → Bool) → ℝ) : Prop

def BooleanFourier.HasBoundedRange {n : ℕ} (f : (Fin n → Bool) → ℝ) : Prop

theorem BooleanFourier.majority_is_stablest_theorem01 (ρ : ℝ) (hρ₀ : 0 < ρ) (hρ₁ : ρ < 1) (ε : ℝ) (hε : 0 < ε) : ∃ δ > 0, ∀ (n : ℕ) (f : (Fin n → Bool) → ℝ), HasBoundedRange01 f → boolExpectation f = 1 / 2 → (∀ (i : Fin n), influenceReal f i ≤ δ) → noiseStability ρ f ≤ halfspaceNoiseStability01 ρ (1 / 2) + ε

theorem BooleanFourier.majority_is_stablest_general (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ < 1) (ε : ℝ) (hε : 0 < ε) : ∃ δ > 0, ∀ (n : ℕ) (f : (Fin n → Bool) → ℝ), HasBoundedRange f → maxInfluence f ≤ δ → noiseStability ρ f ≤ halfspaceNoiseStability ρ (boolExpectation f) + ε