def Discrepancy.boolSign (b : Bool) : ℤ

Convert a Bool to a $\pm 1$ sign: true ↦ 1, false ↦ -1.

@[simp]

theorem Discrepancy.boolSign_true : boolSign true = 1

boolSign true = 1.

@[simp]

theorem Discrepancy.boolSign_false : boolSign false = -1

boolSign false = -1.

theorem Discrepancy.boolSign_not (b : Bool) : (boolSign !b) = -boolSign b

Negating a Boolean flips the sign: boolSign (!b) = -boolSign b.

def Discrepancy.disc {n : ℕ} (f : Fin n → Bool) (S : Finset (Fin n)) : ℤ

The signed discrepancy of a $\pm 1$ coloring f on a set S: $\operatorname{disc}(f, S) = \sum_{i \in S} \operatorname{sign}(f(i))$.

theorem Discrepancy.disc_not {n : ℕ} (f : Fin n → Bool) (S : Finset (Fin n)) : disc (fun (i : Fin n) => !f i) S = -disc f S

Flipping all signs of a coloring negates its discrepancy.

theorem Discrepancy.exp_disc_eq_prod {n : ℕ} (s : ℝ) (S : Finset (Fin n)) (f : Fin n → Bool) : Real.exp (s * ↑(disc f S)) = ∏ i ∈ S, Real.exp (s * ↑(boolSign (f i)))

The exponential of a scaled discrepancy factors as a product over the set: $e^{s \cdot \operatorname{disc}(f, S)} = \prod_{i \in S} e^{s \cdot \operatorname{sign}(f(i))}$.

theorem Discrepancy.exp_moment_eq {n : ℕ} (s : ℝ) (S : Finset (Fin n)) : ∑ f : Fin n → Bool, Real.exp (s * ↑(disc f S)) = 2 ^ n * Real.cosh s ^ S.card

The moment generating function identity for the discrepancy under uniform $\pm 1$ colorings: $\sum_{f \in \{-1,1\}^n} e^{s \cdot \operatorname{disc}(f, S)} = 2^n \cosh(s)^{|S|}$.

theorem Discrepancy.one_sided_chernoff {n : ℕ} (hn : 0 < n) (S : Finset (Fin n)) (t : ℝ) (ht : 0 < t) : ↑{f : Fin n → Bool | t ≤ ↑(disc f S)}.card ≤ 2 ^ n * Real.exp (-(t ^ 2 / (2 * ↑n)))

One-sided Chernoff bound for set discrepancy: the number of $\pm 1$ colorings $f$ with $\operatorname{disc}(f, S) \geq t$ is at most $2^n \exp(-t^2 / (2n))$.

theorem Discrepancy.card_filter_disc_neg {n : ℕ} (S : Finset (Fin n)) (t : ℝ) : {f : Fin n → Bool | ↑(disc f S) ≤ -t}.card = {f : Fin n → Bool | t ≤ ↑(disc f S)}.card

By the sign-flipping involution, the number of colorings with discrepancy $\leq -t$ equals the number with discrepancy $\geq t$.

theorem Discrepancy.two_sided_chernoff {n : ℕ} (hn : 0 < n) (S : Finset (Fin n)) (t : ℝ) (ht : 0 < t) : ↑{f : Fin n → Bool | t ≤ |↑(disc f S)|}.card ≤ 2 ^ (n + 1) * Real.exp (-(t ^ 2 / (2 * ↑n)))

Two-sided Chernoff bound for set discrepancy: the number of $\pm 1$ colorings $f$ with $|\operatorname{disc}(f, S)| \geq t$ is at most $2^{n+1} \exp(-t^2 / (2n))$.

theorem Discrepancy.mul_exp_neg_two_log (m : ℕ) (hm : 0 < m) : ↑m * Real.exp (-(2 * Real.log ↑m)) = 1 / ↑m

Algebraic identity: $m \cdot e^{-2 \log m} = 1/m$ for $m > 0$.

theorem Discrepancy.discrepancy_bound (n : ℕ) (hn : 0 < n) (F : Finset (Finset (Fin n))) (hF : 3 ≤ F.card) : ∃ (f : Fin n → Bool), ∀ S ∈ F, |↑(disc f S)| ≤ 2 * √(↑n * Real.log ↑F.card)

Discrepancy bound (Theorem 5.1.1). For any collection $\mathcal{F}$ of subsets of $[n]$ with $|\mathcal{F}| \geq 3$, there exists a $\pm 1$ coloring $f$ such that $|\operatorname{disc}(f, S)| \leq 2\sqrt{n \log |\mathcal{F}|}$ for every $S \in \mathcal{F}$.