Main results

The main exports use the concrete Proposition 3.1 family and its equation-(9) limits. An independent big-cell proof is available under names ending in _via_big_cell.

Lean Pool port of wewantmoore commit d59bd80ea93fabb9faf769e790ab47692645e022. The port adds a namespace and adapts proofs to the current Mathlib APIs and repository style.

theorem MooreBound.DegreeDiameter.theorem_1_1 {k : ℕ} (hk : 0 < k) : Filter.Tendsto (fun (d : ℕ) => ↑(nKD k d) / ↑d ^ k) Filter.atTop (nhds 1)

Theorem 1.1. For every fixed positive k, the maximum order of a finite simple graph of maximum degree at most d and extended diameter at most k, divided by d^k, tends to one as d tends to infinity.

theorem MooreBound.DegreeDiameter.theorem_1_1_via_big_cell {k : ℕ} (hk : 0 < k) : Filter.Tendsto (fun (d : ℕ) => ↑(nKD k d) / ↑d ^ k) Filter.atTop (nhds 1)

An independent proof of Theorem 1.1 through the big-cell lower bound.

theorem MooreBound.DegreeDiameter.corollary_1_2 {ell : ℕ} (hell : 2 ≤ ell) : 1 ≤ Filter.liminf (fun (d : ℕ) => ↑(h ell d) / ↑d ^ ell) Filter.atTop

Corollary 1.2. For every fixed ell ≥ 2, the lower limit of the edge extremum (with line-graph extended diameter at most ell), normalized by d^ell, is at least one.

theorem MooreBound.DegreeDiameter.corollary_1_2_via_big_cell {ell : ℕ} (hell : 2 ≤ ell) : 1 ≤ Filter.liminf (fun (d : ℕ) => ↑(h ell d) / ↑d ^ ell) Filter.atTop

An independent proof of Corollary 1.2 through the big-cell lower bound.