def UnbalancingLights.boolToSign (b : Bool) : ℤ

Conversion from booleans to signs $\{-1, +1\}$: true ↦ 1, false ↦ -1.

def UnbalancingLights.IsSignVec {n : ℕ} (v : Fin n → ℤ) : Prop

A vector $v : \mathrm{Fin}\,n \to \mathbb{Z}$ is a sign vector if every entry is $\pm 1$.

def UnbalancingLights.IsSignMatrix {m n : ℕ} (a : Fin m → Fin n → ℤ) : Prop

A matrix $a : \mathrm{Fin}\,m \times \mathrm{Fin}\,n \to \mathbb{Z}$ is a sign matrix if every entry is $\pm 1$.

def UnbalancingLights.rademacherAbsExpect (n : ℕ) : ℤ

Total Rademacher absolute expectation: $\sum_{y \in \{-1,+1\}^n} \left| \sum_j y_j \right|$, i.e., the (unnormalized) expected absolute value of a $\pm 1$ random walk of length $n$.

theorem UnbalancingLights.boolToSign_isSign (b : Bool) : boolToSign b = 1 ∨ boolToSign b = -1

The image of boolToSign lies in $\{-1, +1\}$.

theorem UnbalancingLights.isSignVec_boolToSign {n : ℕ} (f : Fin n → Bool) : IsSignVec fun (j : Fin n) => boolToSign (f j)

Mapping a boolean vector pointwise through boolToSign yields a sign vector.

theorem UnbalancingLights.exists_ge_sum_div {ι : Type u_1} [Fintype ι] [Nonempty ι] (f : ι → ℤ) : ∃ (x : ι), ↑(Fintype.card ι) * f x ≥ ∑ y : ι, f y

Averaging principle: for any function $f : \iota \to \mathbb{Z}$ on a finite nonempty type there exists $x \in \iota$ whose value, multiplied by $|\iota|$, exceeds the total sum $\sum_y f(y)$.

theorem UnbalancingLights.bilinear_eq_row_sum {m n : ℕ} (a : Fin m → Fin n → ℤ) (x : Fin m → ℤ) (y : Fin n → ℤ) : ∑ i : Fin m, ∑ j : Fin n, a i j * x i * y j = ∑ i : Fin m, (∑ j : Fin n, a i j * y j) * x i

Rewriting the bilinear form $\sum_{i,j} a_{ij} x_i y_j$ as a row-by-row dot product $\sum_i (\sum_j a_{ij} y_j) x_i$.

theorem UnbalancingLights.exists_sign_mul_eq_abs (z : ℤ) : ∃ (s : ℤ), (s = 1 ∨ s = -1) ∧ s * z = |z|

For every integer $z$, there is a sign $s \in \{-1, +1\}$ with $s \cdot z = |z|$.

theorem UnbalancingLights.greedy_row_selection {m n : ℕ} (a : Fin m → Fin n → ℤ) (y : Fin n → ℤ) : ∃ (x : Fin m → ℤ), IsSignVec x ∧ ∑ i : Fin m, ∑ j : Fin n, a i j * x i * y j = ∑ i : Fin m, |∑ j : Fin n, a i j * y j|

Greedy row selection: given a matrix $a$ and a vector $y$, choose for each row $i$ a sign $x_i \in \{-1, +1\}$ to align with the row-sum, so that $\sum_{i,j} a_{ij} x_i y_j = \sum_i \left|\sum_j a_{ij} y_j\right|$.

def UnbalancingLights.signFlip {n : ℕ} (a : Fin n → ℤ) (y : Fin n → Bool) : Fin n → Bool

Coordinate-wise sign flip on Boolean vectors: flip $y_j$ exactly when $a_j = -1$.

theorem UnbalancingLights.signFlip_involutive {n : ℕ} (a : Fin n → ℤ) : Function.Involutive (signFlip a)

The sign flip operation is its own inverse.

def UnbalancingLights.signFlipEquiv {n : ℕ} (a : Fin n → ℤ) : (Fin n → Bool) ≃ (Fin n → Bool)

The sign-flip operation packaged as an Equiv on Boolean vectors, used to relabel sums over $\{-1, +1\}^n$.

theorem UnbalancingLights.sign_mul_boolToSign (a : ℤ) (ha : a = 1 ∨ a = -1) (b : Bool) : a * boolToSign b = boolToSign (decide (a = -1) ^^ b)

Compatibility: multiplying a sign $a \in \{-1, +1\}$ by boolToSign b is the same as boolToSign applied to the XOR-flipped bit.

theorem UnbalancingLights.sum_abs_row_eq {n : ℕ} (a : Fin n → ℤ) (ha : ∀ (j : Fin n), a j = 1 ∨ a j = -1) : ∑ y : Fin n → Bool, |∑ j : Fin n, a j * boolToSign (y j)| = ∑ y : Fin n → Bool, |∑ j : Fin n, boolToSign (y j)|

Sign-symmetry of the Rademacher-row sum: for any sign row $a$, $\sum_y |\sum_j a_j y_j|$ over $y \in \{-1,+1\}^n$ equals $\sum_y |\sum_j y_j|$, since the sign flip is a bijection on $\{-1,+1\}^n$.

theorem UnbalancingLights.total_sum_eq {n : ℕ} (a : Fin n → Fin n → ℤ) (ha : IsSignMatrix a) : ∑ y : Fin n → Bool, ∑ i : Fin n, |∑ j : Fin n, a i j * boolToSign (y j)| = ↑n * rademacherAbsExpect n

Total sum identity used in the unbalancing-lights proof: for a sign matrix $a$, $\sum_y \sum_i |\sum_j a_{ij} y_j| = n \cdot \mathbb{E}_{\mathrm{Rad}}(n)$, where the right-hand side is the (unnormalized) Rademacher walk expectation.

theorem UnbalancingLights.unbalancing_lights {n : ℕ} (a : Fin n → Fin n → ℤ) (ha : IsSignMatrix a) : ∃ (x : Fin n → ℤ) (y : Fin n → ℤ), IsSignVec x ∧ IsSignVec y ∧ ↑(Fintype.card (Fin n → Bool)) * ∑ i : Fin n, ∑ j : Fin n, a i j * x i * y j ≥ ↑n * rademacherAbsExpect n

Unbalancing lights (Theorem 2.5.1, integer form). For any sign matrix $a \in \{-1, +1\}^{n \times n}$, there exist sign vectors $x, y \in \{-1, +1\}^n$ such that $2^n \cdot \sum_{i,j} a_{ij} x_i y_j \geq n \cdot \mathbb{E}_{\mathrm{Rad}}(n)$. This gives the asymptotic bound $\sum_{i,j} a_{ij} x_i y_j \geq (\sqrt{2/\pi} + o(1)) n^{3/2}$.

def UnbalancingLights.IsCrossEdge {k n : ℕ} (e : Finset (Fin k × Fin n)) : Prop

A "cross edge" in the $k$-partite hypergraph on $\mathrm{Fin}\,k \times \mathrm{Fin}\,n$: a $k$-element set $e$ that picks exactly one vertex from each "part" $\{i\} \times \mathrm{Fin}\,n$.

noncomputable def UnbalancingLights.discrepancy {k n : ℕ} (color : Finset (Fin k × Fin n) → ℤ) (S : Finset (Fin k × Fin n)) : ℝ

Discrepancy of a coloring on $k$-subsets of $S$: the signed sum $\sum_{e \in \binom{S}{k}} \mathrm{color}(e)$ viewed as a real number.

theorem UnbalancingLights.unbalancing_lights_improved (k : ℕ) (hk : 2 ≤ k) : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (color : Finset (Fin k × Fin n) → ℤ), (∀ (e : Finset (Fin k × Fin n)), e.card = k → color e = 1 ∨ color e = -1) → (∀ (e : Finset (Fin k × Fin n)), IsCrossEdge e → color e = 1) → ∃ (S : Finset (Fin k × Fin n)), |discrepancy color S| ≥ c * ↑n ^ k

Improved unbalancing lights (Theorem 2.5.2). For each $k \geq 2$ there is a constant $c > 0$ such that for every $n \geq 1$ and every $\pm 1$ coloring of the $k$-element subsets of $\mathrm{Fin}\,k \times \mathrm{Fin}\,n$ that assigns $+1$ to all cross edges, some sub-hypergraph $S$ has discrepancy at least $c \cdot n^k$ in absolute value.