theorem BooleanFourier.parseval_pm_one {n : ℕ} (f : (Fin n → Bool) → ℝ) (hf : ∀ (x : Fin n → Bool), f x = 1 ∨ f x = -1) : ∑ S : Finset (Fin n), fourierCoeff f S ^ 2 = 1

theorem BooleanFourier.variance_pm_one {n : ℕ} (f : (Fin n → Bool) → ℝ) (hf : ∀ (x : Fin n → Bool), f x = 1 ∨ f x = -1) : ∑ S : Finset (Fin n) with S ≠ ∅, fourierCoeff f S ^ 2 = 1 - fourierCoeff f ∅ ^ 2

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

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

theorem BooleanFourier.totalInfluence_eq_weighted_degree {n : ℕ} (f : (Fin n → Bool) → ℝ) : ∑ S : Finset (Fin n), ↑S.card * fourierCoeff f S ^ 2 = ∑ k ∈ Finset.range (n + 1), ↑k * fourierWeightAtLevel k f

theorem BooleanFourier.low_degree_concentration {n : ℕ} (f : (Fin n → Bool) → ℝ) (hf : ∀ (x : Fin n → Bool), f x = 1 ∨ f x = -1) (K : ℝ) (hK : ∑ S : Finset (Fin n), ↑S.card * fourierCoeff f S ^ 2 ≤ K) (ε : ℝ) (hε : 0 < ε) : ∑ S : Finset (Fin n) with ↑S.card > 2 * K / ε, fourierCoeff f S ^ 2 ≤ ε

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

theorem BooleanFourier.noiseStability_via_weight {n : ℕ} (ρ : ℝ) (f : (Fin n → Bool) → ℝ) : ∑ S : Finset (Fin n), ρ ^ S.card * fourierCoeff f S ^ 2 = ∑ k ∈ Finset.range (n + 1), ρ ^ k * fourierWeightAtLevel k f

theorem BooleanFourier.level_k_inequality {n : ℕ} (ρ : ℝ) (hρ : |ρ| ≤ 1) (k : ℕ) (f : (Fin n → Bool) → ℝ) : fourierWeightUpToLevel k (noiseOperator ρ f) ≤ fourierWeightUpToLevel k f

theorem BooleanFourier.noiseOp_self_adjoint {n : ℕ} (ρ : ℝ) (f g : (Fin n → Bool) → ℝ) : innerProduct (noiseOperator ρ f) g = innerProduct f (noiseOperator ρ g)