Matrix discrepancy

Adapted for Lean Pool by changing module paths and selecting explicit imports.

A colouring is a function with values in {-1, 1}. For a matrix A and a colouring χ, Komlos.colouringDiscrepancy A χ is the supremum norm of A *ᵥ χ. Komlos.discrepancy A is the minimum over all colourings.

Komlos.discrepancy_le_iff expresses a discrepancy bound as the existence of a colouring satisfying that bound. The minimum is attained because there are finitely many colourings.

def Komlos.IsColouring {n : Type u_2} (χ : n → ℝ) : Prop

A colouring of n is a ±1-valued function on n.

Equations

• Komlos.IsColouring χ = ∀ (j : n), χ j = 1 ∨ χ j = -1

def Komlos.ofBool {n : Type u_2} (b : n → Bool) : n → ℝ

The colouring attached to a Boolean assignment.

Equations

• Komlos.ofBool b j = if b j = true then 1 else -1

theorem Komlos.isColouring_ofBool {n : Type u_2} (b : n → Bool) : IsColouring (ofBool b)

theorem Komlos.IsColouring.abs_eq_one {n : Type u_2} {χ : n → ℝ} (hχ : IsColouring χ) (j : n) : |χ j| = 1

theorem Komlos.exists_ofBool_eq {n : Type u_2} {χ : n → ℝ} (hχ : IsColouring χ) : ∃ (b : n → Bool), ofBool b = χ

noncomputable def Komlos.colouringDiscrepancy {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℝ) (χ : n → ℝ) : ℝ

The discrepancy of the colouring χ with respect to A: the supremum norm of the signed sum A *ᵥ χ of the columns of A.

Equations

• Komlos.colouringDiscrepancy A χ = ‖A.mulVec χ‖

noncomputable def Komlos.discrepancy {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℝ) : ℝ

The discrepancy of the matrix A: the least discrepancy of a colouring of its columns.

Equations

• Komlos.discrepancy A = ⨅ (b : n → Bool), Komlos.colouringDiscrepancy A (Komlos.ofBool b)

theorem Komlos.colouringDiscrepancy_le_iff {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] {A : Matrix m n ℝ} {χ : n → ℝ} {C : ℝ} (hC : 0 ≤ C) : colouringDiscrepancy A χ ≤ C ↔ ∀ (i : m), |∑ j : n, A i j * χ j| ≤ C

theorem Komlos.colouringDiscrepancy_nonneg {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℝ) (χ : n → ℝ) : 0 ≤ colouringDiscrepancy A χ

theorem Komlos.colouringDiscrepancy_add_le {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A B : Matrix m n ℝ) (χ : n → ℝ) : colouringDiscrepancy (A + B) χ ≤ colouringDiscrepancy A χ + colouringDiscrepancy B χ

theorem Komlos.colouringDiscrepancy_le_of_abs_le {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] {A : Matrix m n ℝ} {χ : n → ℝ} (hχ : IsColouring χ) {c : ℝ} (hc : 0 ≤ c) (hA : ∀ (i : m) (j : n), |A i j| ≤ c) : colouringDiscrepancy A χ ≤ ↑(Fintype.card n) * c

A matrix whose entries are at most c in absolute value has colouring discrepancy at most c times its number of columns.

theorem Komlos.colouringDiscrepancy_smul {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (c : ℝ) (A : Matrix m n ℝ) (χ : n → ℝ) : colouringDiscrepancy (c • A) χ = |c| * colouringDiscrepancy A χ

theorem Komlos.discrepancy_smul {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (c : ℝ) (A : Matrix m n ℝ) : discrepancy (c • A) = |c| * discrepancy A

theorem Komlos.discrepancy_le_colouringDiscrepancy {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] {A : Matrix m n ℝ} {χ : n → ℝ} (hχ : IsColouring χ) : discrepancy A ≤ colouringDiscrepancy A χ

theorem Komlos.exists_isColouring_colouringDiscrepancy_eq {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m n ℝ) : ∃ (χ : n → ℝ), IsColouring χ ∧ colouringDiscrepancy A χ = discrepancy A

theorem Komlos.discrepancy_le_iff {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] {A : Matrix m n ℝ} {C : ℝ} : discrepancy A ≤ C ↔ ∃ (χ : n → ℝ), IsColouring χ ∧ colouringDiscrepancy A χ ≤ C

The discrepancy of A is at most C exactly when some colouring has discrepancy at most C: the infimum over the finitely many colourings is attained.