theorem BooleanFourier.fourierCoeff_chi_singleton {n : ℕ} (i : Fin n) (S : Finset (Fin n)) : fourierCoeff (chi {i}) S = if S = {i} then 1 else 0

theorem BooleanFourier.chi_comp_perm {k : ℕ} (σ : Equiv.Perm (Fin k)) (S : Finset (Fin k)) (x : Fin k → Bool) : chi S (x ∘ ⇑σ) = chi (Finset.image (⇑σ) S) x

noncomputable def BooleanFourier.vertexAvgFunc {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {k : ℕ} (game : UniqueGames.UniqueGame V W k) (f : W → (Fin k → Bool) → ℝ) (v : V) : (Fin k → Bool) → ℝ

theorem BooleanFourier.fourierCoeff_vertex_avg {V : Type u_1} {W : Type u_2} [DecidableEq V] [DecidableEq W] {k : ℕ} (game : UniqueGames.UniqueGame V W k) (f : W → (Fin k → Bool) → ℝ) (v : V) (S : Finset (Fin k)) : fourierCoeff (vertexAvgFunc game f v) S = 1 / ↑game.left_degree * ∑ e ∈ game.edges with e.1 = v, fourierCoeff (f e.2) (Finset.image (⇑(game.constraint v e.2)) S)

theorem BooleanFourier.noiseStability_chi_singleton {n : ℕ} (ρ : ℝ) (i : Fin n) : noiseStability ρ (chi {i}) = ρ

theorem BooleanFourier.disagreementProb_dictator {n : ℕ} (ρ : ℝ) (i : Fin n) : disagreementProb ρ (chi {i}) = (1 - ρ) / 2