theorem BooleanFourier.fourierCoeff_eq_expectation {n : ℕ} (f : (Fin n → Bool) → ℝ) (S : Finset (Fin n)) : fourierCoeff f S = 1 / 2 ^ n * ∑ x : Fin n → Bool, f x * chi S x

theorem BooleanFourier.abs_chi_eq_one {n : ℕ} (S : Finset (Fin n)) (x : Fin n → Bool) : |chi S x| = 1

theorem BooleanFourier.sample_bounded {n : ℕ} (f : (Fin n → Bool) → ℝ) (S : Finset (Fin n)) (hf : ∀ (x : Fin n → Bool), |f x| ≤ 1) (x : Fin n → Bool) : |f x * chi S x| ≤ 1

theorem BooleanFourier.fourier_sampling_hoeffding_bound {n : ℕ} (f : (Fin n → Bool) → ℝ) (S : Finset (Fin n)) (hf : ∀ (x : Fin n → Bool), |f x| ≤ 1) (ε : ℝ) (hε : 0 < ε) (m : ℕ) (hm : 1 ≤ m) : ↑{samples : Fin m → Fin n → Bool | |1 / ↑m * ∑ i : Fin m, f (samples i) * chi S (samples i) - fourierCoeff f S| ≥ ε}.card / (2 ^ n) ^ m ≤ 2 * Real.exp (-(↑m * ε ^ 2 / 2))

theorem BooleanFourier.claim_1_2_fourier_sampling {n : ℕ} (f : (Fin n → Bool) → ℝ) (S : Finset (Fin n)) (hf : ∀ (x : Fin n → Bool), |f x| ≤ 1) (ε : ℝ) (hε : 0 < ε) (δ : ℝ) (hδ : 0 < δ) (hδ2 : δ ≤ 1) : ∃ (m : ℕ), 1 ≤ m ∧ m ≤ ⌈2 * Real.log (2 / δ) / ε ^ 2⌉₊ ∧ ↑{samples : Fin m → Fin n → Bool | |1 / ↑m * ∑ i : Fin m, f (samples i) * chi S (samples i) - fourierCoeff f S| ≥ ε}.card / (2 ^ n) ^ m ≤ δ