noncomputable def SimpleGraph.maxEccentricityVertices {α : Type u_1} (G : SimpleGraph α) : Set α

The set of vertices of maximum eccentricity.

Equations

• G.maxEccentricityVertices = {v : α | G.eccent v = G.ediam}

noncomputable def SimpleGraph.averageEccentricity {α : Type u_1} [Fintype α] (G : SimpleGraph α) : ℝ

The average eccentricity of a graph G: the mean of G.eccent v over all vertices, converted to a real number. Returns 0 if the graph has no vertices.

Equations

• G.averageEccentricity = ↑(∑ v : α, (G.eccent v).toNat) / ↑(Fintype.card α)

def SimpleGraph.computable_ediam {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ

The diameter of a finite graph as a computable natural number: the maximum BFS distance (computable_dist) over all ordered pairs of vertices.

Equations

• G.computable_ediam = Finset.univ.sup fun (p : α × α) => G.computable_dist p.1 p.2

theorem SimpleGraph.ediam_eq_computable {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] [Nonempty α] (hc : G.Connected) : G.ediam = ↑G.computable_ediam

For a connected finite graph, the extended diameter ediam equals the computable diameter.

def SimpleGraph.computable_eccent {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (u : α) : ℕ

The eccentricity of a vertex u in a finite graph as a computable natural number: the maximum BFS distance (computable_dist) from u to any vertex.

Equations

• G.computable_eccent u = Finset.univ.sup fun (v : α) => G.computable_dist u v

def SimpleGraph.computable_radius {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] [Nonempty α] : ℕ

The radius of a finite graph as a computable natural number: the minimum, over all vertices, of the computable eccentricity.

Equations

• G.computable_radius = Finset.univ.inf' ⋯ G.computable_eccent

theorem SimpleGraph.eccent_eq_computable {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] [Nonempty α] (hc : G.Connected) (u : α) : G.eccent u = ↑(G.computable_eccent u)

For a connected finite graph, the eccentricity eccent u equals the computable eccentricity.

theorem SimpleGraph.radius_eq_computable {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] [Nonempty α] (hc : G.Connected) : G.radius = ↑G.computable_radius

For a connected finite graph, the radius radius equals the computable radius.