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

theorem BooleanFourier.noiseOperator_eq_fourier_sum {n : ℕ} (ρ : ℝ) (f : (Fin n → Bool) → ℝ) (x : Fin n → Bool) : noiseOperator ρ f x = ∑ S : Finset (Fin n), ρ ^ S.card * fourierCoeff f S * chi S x

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

theorem BooleanFourier.sum_chi_mul_chi_eq {n : ℕ} (S T : Finset (Fin n)) : ∑ x : Fin n → Bool, chi S x * chi T x = if S = T then 2 ^ n else 0

theorem BooleanFourier.noiseStability_eq_sum {n : ℕ} (ρ : ℝ) (f : (Fin n → Bool) → ℝ) : noiseStability ρ f = ∑ S : Finset (Fin n), ρ ^ S.card * fourierCoeff f S ^ 2

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

theorem BooleanFourier.lpNorm_four_pow_le_of_degree {n : ℕ} (f : BoolFn n) (d : ℕ) (hdeg : ∀ (S : Finset (Fin n)), S.card > d → fourierCoeff f S = 0) : lpNorm 4 f ^ 4 ≤ 9 ^ d * lpNorm 2 f ^ 4

theorem BooleanFourier.lpNorm_rpow_eq {n : ℕ} (f : BoolFn n) {p : ℝ} (hp : 0 < p) : lpNorm p f ^ p = 1 / 2 ^ n * ∑ x : Fin n → Bool, |f x| ^ p

theorem BooleanFourier.anticoncentration_thm38 {n : ℕ} (f : BoolFn n) (d : ℕ) (hdeg : ∀ (S : Finset (Fin n)), S.card > d → fourierCoeff f S = 0) (θ : ℝ) (hθ0 : 0 < θ) (hθ1 : θ < 1) : ↑{x : Fin n → Bool | |f x| ≥ θ * lpNorm 2 f}.card / 2 ^ n ≥ (1 - θ ^ 2) ^ 2 / 9 ^ d

theorem BooleanFourier.degree_le_iff {n : ℕ} (f : BoolFn n) (d : ℕ) : degree f ≤ d ↔ ∀ (S : Finset (Fin n)), S.card > d → fourierCoeff f S = 0

theorem BooleanFourier.anticoncentration_low_degree {n : ℕ} (f : BoolFn n) (hf01 : ∀ (x : Fin n → Bool), f x = 0 ∨ f x = 1) (δ : ℝ) (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1) (hδ_eq : ↑{x : Fin n → Bool | f x = 1}.card / 2 ^ n = δ) : ↑(degree f) ≥ Real.log (1 / δ) / Real.log 9