noncomputable def SimpleGraph.averageDegree {α : Type u_1} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] : ℚ

The average degree of G.

Equations

• G.averageDegree = (∑ v : α, ↑(G.degree v)) / ↑(Fintype.card α)

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

The multiset of degrees of a graph.

Equations

• G.degreeMultiset = Multiset.map (fun (v : α) => G.degree v) Finset.univ.val

noncomputable def SimpleGraph.degreeSequence {α : Type u_1} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] : List ℕ

The degree sequence of a graph, sorted in nondecreasing order.

Equations

• G.degreeSequence = (Multiset.map (fun (v : α) => G.degree v) Finset.univ.val).sort fun (x1 x2 : ℕ) => x1 ≤ x2

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

The maximum number of occurrences of any term of the degree sequence of G.

Equations

• G.degreeSequenceMultiplicity = (List.map (fun (d : ℕ) => List.count d G.degreeSequence) G.degreeSequence).max?.getD 0

noncomputable def SimpleGraph.edegree {V : Type u_2} (G : SimpleGraph V) (v : V) : ℕ∞

Infinite graphs: definitions for max degree and clique number so that the maximum degree of a graph with unbounded degree is ∞ rather than 0.

Equations

• G.edegree v = (G.neighborSet v).encard

noncomputable def SimpleGraph.emaxDegree {V : Type u_2} (G : SimpleGraph V) : ℕ∞

Equations

• G.emaxDegree = ⨆ (v : V), G.edegree v

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 α) : ℝ

Equations

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

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

The second-smallest degree of G's degree sequence — DeLaVina's σ(G) per the WOWII definitions popup (defEntry 65): "order the degree sequence in nondecreasing order d₁ ≤ d₂ ≤ … ≤ dₙ, the second smallest degree of the sequence is the 2nd entry". For graphs with n ≤ 1 we conventionally return 0.

Equations

• G.secondSmallestDegree = G.degreeSequence.getD 1 0

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

The number of triangles (3-cliques) of G incident to vertex v: the number of 3-element cliques containing v.

Equations

• G.numTrianglesAtVertex v = {s ∈ G.cliqueFinset 3 | v ∈ s}.card

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

The length of a graph: the square root of the sum of the squares of degrees.

Equations

• G.degreeL2Norm = √(∑ v : α, ↑(G.degree v) ^ 2)

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

The number of vertices of degree k in G.

Equations

• G.countDegreeK k = {v : α | G.degree v = k}.card