theorem BooleanFourier.fourierInfluence_eq_influenceReal {n : ℕ} (f : (Fin n → Bool) → ℝ) (i : Fin n) : fourierInfluence f i = influenceReal f i

theorem BooleanFourier.fourierInfluence_liftPM_eq_influence {n : ℕ} (f : (Fin n → Bool) → Bool) (i : Fin n) : fourierInfluence (liftPM f) i = influence f i

theorem BooleanFourier.influence_lt_of_not_mem_highInfluenceCoords {n : ℕ} (f : (Fin n → Bool) → Bool) (τ : ℝ) (i : Fin n) (hi : i ∉ highInfluenceCoords f τ) : influence f i < τ

theorem BooleanFourier.fourierInfluence_lt_of_not_mem_J {n : ℕ} (f : (Fin n → Bool) → Bool) (τ : ℝ) (i : Fin n) (hi : i ∉ highInfluenceCoords f τ) : fourierInfluence (liftPM f) i < τ

theorem BooleanFourier.fourierCoeff_sq_lt_of_not_subset_J {n : ℕ} (f : (Fin n → Bool) → Bool) (τ : ℝ) (S : Finset (Fin n)) (hS : ¬S ⊆ highInfluenceCoords f τ) : fourierCoeff (liftPM f) S ^ 2 < τ

theorem BooleanFourier.log_inv_pos_of_tau {τ : ℝ} (hτ0 : 0 < τ) (hτ1 : τ < 1) : Real.log (1 / τ) > 0

theorem BooleanFourier.spectral_entropy_le_two_totalInfluence {n : ℕ} (f : (Fin n → Bool) → Bool) : ∑ S : Finset (Fin n) with fourierCoeff (liftPM f) S ≠ 0, fourierCoeff (liftPM f) S ^ 2 * Real.log (1 / fourierCoeff (liftPM f) S ^ 2) ≤ 2 * totalInfluence f

theorem BooleanFourier.fourierCoeff_sq_le_one_of_liftPM {n : ℕ} (f : (Fin n → Bool) → Bool) (S : Finset (Fin n)) : fourierCoeff (liftPM f) S ^ 2 ≤ 1

theorem BooleanFourier.friedgut_weighted_fourier_bound {n : ℕ} (f : (Fin n → Bool) → Bool) (τ : ℝ) (hτ0 : 0 < τ) (hτ1 : τ < 1) : (∑ S : Finset (Fin n) with ¬S ⊆ highInfluenceCoords f τ, fourierCoeff (liftPM f) S ^ 2) * Real.log (1 / τ) ≤ 2 * totalInfluence f

theorem BooleanFourier.friedgut_tight_concentration {n : ℕ} (f : (Fin n → Bool) → Bool) (τ : ℝ) (hτ0 : 0 < τ) (hτ1 : τ < 1) : ∑ S : Finset (Fin n) with ¬S ⊆ highInfluenceCoords f τ, fourierCoeff (liftPM f) S ^ 2 ≤ 2 * totalInfluence f / Real.log (1 / τ)