/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import Mathlib.Combinatorics.SimpleGraph.Diam
public import Mathlib.Data.Real.Basic
public import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.VertexDistance@[expose] public sectionnamespace SimpleGraphvariable {α : Type*} [Fintype α] [DecidableEq α]The set of vertices of maximum eccentricity.
noncomputable def maxEccentricityVertices (G : SimpleGraph α) : Set α :=
{v : α | G.eccent v = G.ediam}
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.
noncomputable def averageEccentricity (G : SimpleGraph α) : ℝ :=
(∑ v : α, (G.eccent v).toNat) / (Fintype.card α : ℝ)
The diameter of a finite graph as a computable natural number: the maximum BFS distance
(computable_dist) over all ordered pairs of vertices.
def computable_ediam (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
Finset.univ.sup fun p : α × α => computable_dist G p.1 p.2
For a connected finite graph, the extended diameter ediam equals the computable diameter.
α:Type u_1inst✝³:Fintype αinst✝²:DecidableEq αG:SimpleGraph αinst✝¹:DecidableRel G.Adjinst✝:Nonempty αhc:G.Connectedp:α × αhp:(Finset.univ.sup fun p ↦ G.computable_dist p.1 p.2) = G.computable_dist p.1 p.2hp':G.computable_ediam = G.computable_dist p.1 p.2⊢ G.edist p.1 p.2 ≤ G.ediam
All goals completed! 🐙
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.
def computable_eccent (G : SimpleGraph α) [DecidableRel G.Adj] (u : α) : ℕ :=
Finset.univ.sup fun v => computable_dist G u vThe radius of a finite graph as a computable natural number: the minimum, over all vertices, of the computable eccentricity.
def computable_radius (G : SimpleGraph α) [DecidableRel G.Adj] [Nonempty α] : ℕ :=
Finset.univ.inf' Finset.univ_nonempty (computable_eccent G)
For a connected finite graph, the eccentricity eccent u equals the computable eccentricity.
α:Type u_1inst✝³:Fintype αinst✝²:DecidableEq αG:SimpleGraph αinst✝¹:DecidableRel G.Adjinst✝:Nonempty αhc:G.Connectedu:αv:αhv:(Finset.univ.sup fun v ↦ G.computable_dist u v) = G.computable_dist u vhv':G.computable_eccent u = G.computable_dist u v⊢ G.edist u v ≤ G.eccent u
All goals completed! 🐙
For a connected finite graph, the radius radius equals the computable radius.
α:Type u_1inst✝³:Fintype αinst✝²:DecidableEq αG:SimpleGraph αinst✝¹:DecidableRel G.Adjinst✝:Nonempty αhc:G.Connectedu1:αhu1:G.eccent u1 = G.radius⊢ ↑G.computable_radius ≤ ↑(G.computable_eccent u1)
All goals completed! 🐙end SimpleGraph