The Johnson bound for the independence number of the Johnson graph (Erdős Problem 835)

An independent set of the Johnson graph J(n, k) is a family of k-subsets of Fin n pairwise meeting in at most k - 2 points, that is, a constant-weight binary code of distance 4. Johnson's bound α(J(n, k)) ≤ johnsonBound n 4 k is proved by recursion on (n, k): double counting the pairs (point, member) and shortening the members through a point. Definitions and statement are copied verbatim from formal-conjectures.

Main results

• Erdos835.indepNum_johnson_le_johnsonBound: α(J(n, k)) ≤ johnsonBound n 4 k (Johnson 1962; formal-conjectures, Erdős Problem 835)
• Erdos835.card_le_johnsonBound: a family of w-subsets of Fin n pairwise meeting in ≤ w - 2 points has at most johnsonBound n 4 w members

References

• S. M. Johnson, «A new upper bound for error-correcting codes», IRE Trans. Inform. Theory 8 (1962) 203–207.
• erdosproblems.com/835; definitions and statement copied verbatim from google-deepmind/formal-conjectures (ErdosProblems/835.lean and FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Johnson.lean).

theorem Finset.card_lt_card_iff_of_subset {α : Type u_1} {s t : Finset α} (hst : s ⊆ t) : s.card < t.card ↔ s ≠ t

def SimpleGraph.johnson (n k : ℕ) : SimpleGraph { s : Finset (Fin n) // s.card = k }

The Johnson graph $J(n, k)$ has as vertices the $k$-subsets of an $n$-set. Two vertices are adjacent if their intersection has size $k - 1$.

Equations

• SimpleGraph.johnson n k = { Adj := fun (s t : { s : Finset (Fin n) // s.card = k }) => (↑s ∩ ↑t).card + 1 = k, symm := ⋯, loopless := ⋯ }

theorem SimpleGraph.johnson_adj (n k : ℕ) (s t : { s : Finset (Fin n) // s.card = k }) : (johnson n k).Adj s t = ((↑s ∩ ↑t).card + 1 = k)

def SimpleGraph.«termJ(_,_)» : Lean.ParserDescr

Equations

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

def SimpleGraph.«termα(_)» : Lean.ParserDescr

The maximal number of vertices of an independent set in a graph G.

Equations

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

theorem SimpleGraph.johnson_adj_iff_ge {n k : ℕ} {s t : { s : Finset (Fin n) // s.card = k }} : (johnson n k).Adj s t ↔ s ≠ t ∧ k ≤ (↑s ∩ ↑t).card + 1

theorem SimpleGraph.not_johnson_adj_iff_lt {n k : ℕ} {s t : { s : Finset (Fin n) // s.card = k }} : ¬(johnson n k).Adj s t ↔ s = t ∨ (↑s ∩ ↑t).card + 1 < k

def Erdos835.johnsonBound : ℕ → ℕ → ℕ → ℕ

Johnson's upper bound on the maximum size A(n, d, w) of a n-dimensional binary code of distance d and weight w is as follows:

• If d > 2 * w, then A(n, d, w) = 1.
• If d ≤ 2 * w, then A(n, d, w) ≤ ⌊n / w * A(n - 1, d, w - 1)⌋.

Equations

• Erdos835.johnsonBound 0 x✝¹ x✝ = 1
• Erdos835.johnsonBound x✝¹ x✝ 0 = 1
• Erdos835.johnsonBound n.succ x✝ w.succ = if 2 * (w + 1) < x✝ then 1 else (n + 1) * Erdos835.johnsonBound n x✝ w / (w + 1)

Proof

theorem Erdos835.card_le_johnsonBound (n w : ℕ) (C : Finset (Finset (Fin n))) : (∀ s ∈ C, s.card = w) → (∀ s ∈ C, ∀ t ∈ C, s ≠ t → (s ∩ t).card + 2 ≤ w) → C.card ≤ johnsonBound n 4 w

Johnson's bound for constant-weight families with pairwise intersections ≤ w - 2.

theorem Erdos835.indepNum_johnson_le_johnsonBound {n k : ℕ} : (SimpleGraph.johnson n k).indepNum ≤ johnsonBound n 4 k

Johnson's bound for the independence number of the Johnson graph.