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

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

theorem BooleanFourier.monotone_fourierCoeff_singleton_nonneg {n : ℕ} (f : (Fin n → Bool) → Bool) (hf : IsMonotone f) (i : Fin n) : 0 ≤ fourierCoeff (fun (x : Fin n → Bool) => boolToReal (f x)) {i}

theorem BooleanFourier.spectral_sample_expected_cardinality {n : ℕ} (f : (Fin n → Bool) → ℝ) : ∑ S : Finset (Fin n), ↑S.card * fourierCoeff f S ^ 2 = ∑ i : Fin n, fourierInfluence f i

theorem BooleanFourier.noiseSensitivity_dictator {n : ℕ} (hn : 0 < n) (δ : ℝ) : (noiseSensitivity δ fun (x : Fin n → Bool) => x ⟨0, hn⟩) = δ

theorem BooleanFourier.noiseSensitivity_le_totalInfluence_mul_delta {n : ℕ} (f : (Fin n → Bool) → Bool) (δ : ℝ) (_hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1 / 2) : noiseSensitivity δ f ≤ δ * totalInfluence f

theorem GaussianStability.gaussianNoiseStability_mono {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (ρ₁ ρ₂ : ℝ) (hρ₁ : 0 ≤ ρ₁) (hρ₁' : ρ₁ ≤ 1) (hρ₂ : 0 ≤ ρ₂) (hρ₂' : ρ₂ ≤ 1) (hle : ρ₁ ≤ ρ₂) : gaussianNoiseStability ρ₁ hρ₁ hρ₁' f ≤ gaussianNoiseStability ρ₂ hρ₂ hρ₂' f

theorem GaussianStability.gaussianNoiseStability_balanced_halfspace (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) : (gaussianNoiseStability ρ hρ₀ hρ₁ fun (x : EuclideanSpace ℝ (Fin 1)) => if x.ofLp ⟨0, Nat.zero_lt_one⟩ ≥ 0 then 1 else -1) = 2 / Real.pi * Real.arcsin ρ