The Beck–Fiala bound

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

If every vertex of a finite hypergraph belongs to at most t edges, each column of its incidence matrix has Euclidean norm at most √t. The scaled Komlós bound therefore gives an edge discrepancy bound of 36 * √t.

Hypergraph.incidenceMatrix has rows indexed by edges and columns indexed by vertices. Hypergraph.discrepancy_incidenceMatrix_le proves the matrix bound; Hypergraph.exists_isColouring_forall_abs_finsum_le states it as a vertex colouring.

theorem Hypergraph.edgeSet_finite {α : Type u_1} {H : Hypergraph α} (hV : H.vertexSet.Finite) : H.edgeSet.Finite

A hypergraph with finitely many vertices has finitely many edges.

noncomputable def Hypergraph.incidenceMatrix {α : Type u_1} (H : Hypergraph α) (hV : H.vertexSet.Finite) : Matrix ↥⋯.toFinset ↥hV.toFinset ℝ

The incidence matrix of a hypergraph with finitely many vertices: its rows are indexed by the edges, its columns by the vertices, and an entry is 1 when the vertex lies in the edge and 0 otherwise.

Equations

• H.incidenceMatrix hV = Matrix.of fun (e : ↥⋯.toFinset) (x : ↥hV.toFinset) => if ↑x ∈ ↑e then 1 else 0

theorem Hypergraph.incidenceMatrix_apply {α : Type u_1} {H : Hypergraph α} (hV : H.vertexSet.Finite) (e : ↥⋯.toFinset) (x : ↥hV.toFinset) : H.incidenceMatrix hV e x = if ↑x ∈ ↑e then 1 else 0

theorem Hypergraph.sum_incidenceMatrix_sq {α : Type u_1} {H : Hypergraph α} (hV : H.vertexSet.Finite) (x : ↥hV.toFinset) : ∑ e : ↥⋯.toFinset, H.incidenceMatrix hV e x ^ 2 = ↑{e : Set α | e ∈ H.edgeSet ∧ ↑x ∈ e}.ncard

The squared entries of a column of the incidence matrix count the edges containing the vertex.

theorem Hypergraph.discrepancy_incidenceMatrix_le {α : Type u_1} {H : Hypergraph α} {t : ℕ} (hV : H.vertexSet.Finite) (hdeg : ∀ x ∈ H.vertexSet, {e : Set α | e ∈ H.edgeSet ∧ x ∈ e}.ncard ≤ t) : Komlos.discrepancy (H.incidenceMatrix hV) ≤ 36 * √↑t

The Beck–Fiala conjecture, with constant 36: if every vertex of a hypergraph lies in at most t edges, then its incidence matrix has discrepancy at most 36 * √t.

theorem Hypergraph.exists_isColouring_forall_abs_finsum_le {α : Type u_1} {H : Hypergraph α} {t : ℕ} (hV : H.vertexSet.Finite) (hdeg : ∀ x ∈ H.vertexSet, {e : Set α | e ∈ H.edgeSet ∧ x ∈ e}.ncard ≤ t) : ∃ (χ : α → ℝ), Komlos.IsColouring χ ∧ ∀ e ∈ H.edgeSet, |∑ᶠ (x : α) (_ : x ∈ e), χ x| ≤ 36 * √↑t

The Beck–Fiala conjecture, colouring form: if every vertex of a hypergraph lies in at most t edges, then some colouring of the vertices gives every edge discrepancy at most 36 * √t.