Spheres and balls in graphs of bounded degree

The extended distance SimpleGraph.edist changes by at most one along an edge (SimpleGraph.Adj.edist_le_edist_add_one), and a vertex at distance k + 1 from u has a neighbour at distance k, the penultimate vertex of a shortest walk (SimpleGraph.exists_adj_edist_eq_of_edist_eq_add_one).

In a finite graph of maximum degree D, a vertex at positive distance d + 1 from u therefore has at most D - 1 neighbours at distance d + 2, so the sphere of radius d + 1 around u has at most D (D - 1) ^ d vertices (SimpleGraph.card_edist_eq_add_one_le), and the closed ball of radius r at most (D + 1) ^ r (SimpleGraph.card_edist_le_le). The closed ball {v | G.edist u v ≤ r} is the open ball G.ball u (r + 1) of Mathlib.

Main results

• SimpleGraph.Adj.edist_le_edist_add_one: distances change by at most one along an edge.
• SimpleGraph.exists_adj_edist_eq_of_edist_eq_add_one: a vertex at distance k + 1 has a neighbour at distance k.
• SimpleGraph.card_edist_eq_add_one_le: the sphere bound D (D - 1) ^ d.
• SimpleGraph.card_edist_le_le: the ball bound (D + 1) ^ r.

theorem SimpleGraph.Adj.edist_le_edist_add_one {V : Type u_1} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) (w : V) : G.edist u w ≤ G.edist v w + 1

Adjacent vertices have extended distances to any vertex differing by at most one.

theorem SimpleGraph.exists_adj_edist_eq_of_edist_eq_add_one {V : Type u_1} {G : SimpleGraph V} {u w : V} {k : ℕ} (h : G.edist u w = ↑k + 1) : ∃ (v : V), G.Adj v w ∧ G.edist u v = ↑k

A vertex at extended distance k + 1 from u has a neighbour at distance k from u: the penultimate vertex of a shortest walk.

theorem SimpleGraph.card_edist_eq_add_one_le {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] {D : ℕ} (hD : ∀ (v : V), G.degree v ≤ D) (u : V) (d : ℕ) : {v : V | G.edist u v = ↑d + 1}.card ≤ D * (D - 1) ^ d

In a graph of maximum degree D, the sphere of radius d + 1 around a vertex has at most D (D - 1) ^ d vertices.

theorem SimpleGraph.card_edist_le_le {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] {D : ℕ} (hD : ∀ (v : V), G.degree v ≤ D) (u : V) (r : ℕ) : {v : V | G.edist u v ≤ ↑r}.card ≤ (D + 1) ^ r

In a graph of maximum degree D, the closed ball of radius r around a vertex has at most (D + 1) ^ r vertices.