@[reducible, inline]

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

Abbreviation for the average independence number of the neighborhoods.

Equations

• G.l = G.averageIndepNeighbors

@[reducible, inline]

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

The same quantity under a different name, used in some conjectures.

Equations

• G.l_avg = G.averageIndepNeighbors

noncomputable def SimpleGraph.gi {α : Type u_1} (G : SimpleGraph α) : ℕ

Independent domination number of G.

Equations

• G.gi = G.indepDominationNumber

noncomputable def SimpleGraph.temp_v {α : Type u_1} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] (v : α) : ℝ

temp_v G v = deg(v)/(n(G) - deg(v)).

Equations

• G.temp_v v = if Fintype.card α = G.degree v then 0 else ↑(G.degree v) / (↑(Fintype.card α) - ↑(G.degree v))

noncomputable def SimpleGraph.MaxTemp {α : Type u_1} (G : SimpleGraph α) [DecidableRel G.Adj] [Fintype α] [Nonempty α] : ℝ

Maximum of temp_v over all vertices.

Equations

• G.MaxTemp = (Finset.image G.temp_v Finset.univ).max' ⋯

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

Cardinality of the union of the neighbourhoods of the ends of the non-edge e.

Equations

• G.non_edge_neighborhood_card e = Sym2.lift ⟨fun (u v : α) => (G.neighborFinset u ∪ G.neighborFinset v).card, ⋯⟩ e

noncomputable def SimpleGraph.NG {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] : ℝ

Minimum size of the neighbourhood of a non-edge of G.

Equations

• G.NG = if h : Gᶜ.edgeFinset.Nonempty then let neighbor_sizes := Finset.image G.non_edge_neighborhood_card Gᶜ.edgeFinset; ↑(neighbor_sizes.min' ⋯) else ↑(Fintype.card α)

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

Size of a largest induced forest of G expressed as a real number.

Equations

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

noncomputable def SimpleGraph.local_eccentricity {α : Type u_1} (G : SimpleGraph α) (v : α) : ℕ∞

Local eccentricity of a vertex.

Equations

• G.local_eccentricity v = sSup (Set.range (G.edist v))

noncomputable def SimpleGraph.FLOOR (x : ℝ) : ℝ

The largest integer less than or equal to x.

Equations

• SimpleGraph.FLOOR x = ↑⌊x⌋

noncomputable def SimpleGraph.eccentricity {α : Type u_1} (G : SimpleGraph α) (v : α) : ℕ∞

Eccentricity of a vertex.

Equations

• G.eccentricity v = sSup (Set.range (G.edist v))

noncomputable def SimpleGraph.minEccentricity {α : Type u_1} (G : SimpleGraph α) : ℕ∞

The minimum eccentricity among all vertices.

Equations

• G.minEccentricity = sInf (Set.range G.eccentricity)

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

The set of vertices of minimum eccentricity.

Equations

• G.graphCenter = {v : α | G.eccentricity v = G.minEccentricity}

noncomputable def SimpleGraph.maxEccentricity {α : Type u_1} (G : SimpleGraph α) : ℕ∞

The maximum eccentricity among all vertices.

Equations

• G.maxEccentricity = sSup (Set.range G.eccentricity)

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

The set of vertices of maximum eccentricity.

Equations

• G.maxEccentricityVertices = {v : α | G.eccentricity v = G.maxEccentricity}

noncomputable def SimpleGraph.distToSet {α : Type u_1} [Fintype α] (G : SimpleGraph α) (v : α) (S : Set α) : ℕ

Distance from a vertex to a finite set.

Equations

• G.distToSet v S = if h : S.toFinset.Nonempty then (Finset.image (fun (s : α) => G.dist v s) S.toFinset).min' ⋯ else 0

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

Average distance of G.

Equations

• G.averageDistance = if Fintype.card α > 1 then (∑ u : α, ∑ v : α, ↑(G.dist u v)) / (↑(Fintype.card α) * (↑(Fintype.card α) - 1)) else 0

noncomputable def SimpleGraph.path {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) : ℕ

The floor of the average distance of G.

Equations

• G.path = if G.Connected then ⌊G.averageDistance⌋₊ else 0

noncomputable def SimpleGraph.ecc {α : Type u_1} [Fintype α] (G : SimpleGraph α) (S : Set α) : ℕ

Auxiliary quantity ecc used in conjecture 34.

Equations

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

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

Average distance from all vertices to a given set.

Equations

• G.distavg S = if Fintype.card α > 0 then (∑ v : α, ↑(G.distToSet v S)) / ↑(Fintype.card α) else 0

def SimpleGraph.IsPathCover {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) (P : Finset (Finset α)) : Prop

A family of paths covering all vertices without overlaps.

Equations

• G.IsPathCover P = ((∀ s1 ∈ P, ∀ s2 ∈ P, s1 ≠ s2 → Disjoint s1 s2) ∧ Finset.univ ⊆ P.biUnion id ∧ ∀ s ∈ P, ∃ (u : α) (v : α) (p : G.Walk u v), p.IsPath ∧ s = p.support.toFinset)

noncomputable def SimpleGraph.pathCoverNumber {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) : ℕ

Minimum size of a path cover of G.

Equations

• G.pathCoverNumber = sInf {k : ℕ | ∃ (P : Finset (Finset α)), P.card = k ∧ G.IsPathCover P}

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

The same quantity as a real number.

Equations

• G.p = ↑G.pathCoverNumber