def BooleanFourier.IsBoolFnJunta {n : ℕ} (g : (Fin n → Bool) → Bool) (J : ℕ) : Prop

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

def BooleanFourier.restrictToCoords {n : ℕ} (f : (Fin n → Bool) → Bool) (J : Finset (Fin n)) : (Fin n → Bool) → Bool

theorem BooleanFourier.isBoolFnJunta_restrictToCoords {n : ℕ} (f : (Fin n → Bool) → Bool) (J : Finset (Fin n)) : IsBoolFnJunta (restrictToCoords f J) J.card

theorem BooleanFourier.log_two_gt_half : 1 / 2 < Real.log 2

theorem BooleanFourier.le_rpow_two_of_nonneg (x : ℝ) (hx : 0 ≤ x) : x ≤ 2 ^ x

noncomputable def BooleanFourier.fourierTrunc {n : ℕ} (f : (Fin n → Bool) → ℝ) (J : Finset (Fin n)) (x : Fin n → Bool) : ℝ

noncomputable def BooleanFourier.fourierTruncBool {n : ℕ} (f : (Fin n → Bool) → Bool) (J : Finset (Fin n)) : (Fin n → Bool) → Bool

theorem BooleanFourier.isBoolFnJunta_fourierTruncBool {n : ℕ} (f : (Fin n → Bool) → Bool) (J : Finset (Fin n)) : IsBoolFnJunta (fourierTruncBool f J) J.card

theorem BooleanFourier.sign_rounding_sq_bound (a r : ℝ) (ha : a = 1 ∨ a = -1) : (a - if 0 ≤ r then 1 else -1) ^ 2 ≤ 4 * (a - r) ^ 2

theorem BooleanFourier.liftPM_values {n : ℕ} (f : (Fin n → Bool) → Bool) (x : Fin n → Bool) : liftPM f x = 1 ∨ liftPM f x = -1

theorem BooleanFourier.lpNorm_two_eq_sqrt {n : ℕ} (h : (Fin n → Bool) → ℝ) : lpNorm 2 h = √(1 / 2 ^ n * ∑ x : Fin n → Bool, h x ^ 2)

theorem BooleanFourier.fourierCoeff_of_chi_sum {n : ℕ} (F : Finset (Finset (Fin n))) (c : Finset (Fin n) → ℝ) (S : Finset (Fin n)) : fourierCoeff (fun (x : Fin n → Bool) => ∑ T ∈ F, c T * chi T x) S = if S ∈ F then c S else 0

theorem BooleanFourier.friedgut_l2_bridge {n : ℕ} (f : (Fin n → Bool) → Bool) (J : Finset (Fin n)) : ∃ (g : (Fin n → Bool) → Bool), IsBoolFnJunta g J.card ∧ boolL2Dist f g ≤ 2 * √(∑ S : Finset (Fin n) with ¬S ⊆ J, fourierCoeff (liftPM f) S ^ 2)