Basic definitions for the hypergraph lower bound

Basic definitions and the substitution theorem for the hypergraph lower bound.

Hypergraph definitions

@[reducible, inline]

abbrev HypergraphLowerBound.Hypergraph (V : Type u_1) : Type u_1

A finite hypergraph on V, encoded by its finite edge family.

Equations

• HypergraphLowerBound.Hypergraph V = Finset (Finset V)

@[reducible, inline]

abbrev HypergraphLowerBound.HypergraphFamily (ι : Type u_1) (V : Type u_2) : Type (max u_1 u_2)

A family of hypergraphs indexed by ι.

Equations

• HypergraphLowerBound.HypergraphFamily ι V = (ι → HypergraphLowerBound.Hypergraph V)

noncomputable def HypergraphLowerBound.vertexSet {V : Type u_1} [DecidableEq V] (edges : Hypergraph V) : Finset V

The vertex set of a hypergraph given by its edge set: the union of all edges.

Equations

• HypergraphLowerBound.vertexSet edges = Finset.biUnion edges id

noncomputable def HypergraphLowerBound.uniqueCoverage {V : Type u_1} [DecidableEq V] (edges P : Hypergraph V) : ℕ

The unique coverage count: the number of vertices belonging to exactly one edge in P.

Equations

• HypergraphLowerBound.uniqueCoverage edges P = {v ∈ HypergraphLowerBound.vertexSet edges | {e ∈ P | v ∈ e}.card = 1}.card

def HypergraphLowerBound.NoLargePartition {V : Type u_1} [DecidableEq V] (edges : Hypergraph V) (n : ℕ) : Prop

A hypergraph contains no partition of size greater than n.

Equations

• HypergraphLowerBound.NoLargePartition edges n = ∀ P ⊆ edges, HypergraphLowerBound.uniqueCoverage edges P ≤ n

noncomputable def HypergraphLowerBound.H (n : ℕ) : ℕ

H n is the largest number of vertices of a finite hypergraph with no isolated vertices and no partition of size greater than n.

In this development hypergraphs are encoded by their edge sets, so "no isolated vertices" is reflected by taking the vertex set to be the union of the edges.

Equations

• One or more equations did not get rendered due to their size.

The benchmark sequence k_n

@[irreducible]

def HypergraphLowerBound.k : ℕ → ℕ

The benchmark sequence k(n) defined by k(1) = 1 and k(n) = ⌊n/2⌋ + k(⌊n/2⌋) + k(⌊(n+1)/2⌋) for n ≥ 2.

Equations

• HypergraphLowerBound.k 0 = 0
• HypergraphLowerBound.k 1 = 1
• HypergraphLowerBound.k n.succ.succ = (n + 2) / 2 + HypergraphLowerBound.k ((n + 2) / 2) + HypergraphLowerBound.k ((n + 3) / 2)

theorem HypergraphLowerBound.partition_iff_uniqueCoverage {V : Type u_1} [DecidableEq V] (edges : Hypergraph V) (n : ℕ) : NoLargePartition edges n ↔ ∀ P ⊆ edges, uniqueCoverage edges P ≤ n

The partition problem is equivalent to bounding unique coverage.