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

Ls G is the maximum number of leaves over all spanning trees of G. It is defined to be 0 when G is not connected.

Equations

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

noncomputable def SimpleGraph.n {α : Type u_1} [Fintype α] : SimpleGraph α → ℝ

n G is the number of vertices of G as a real number.

Equations

• x✝.n = ↑(Fintype.card α)

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

m G is the size of a maximum matching of G.

Equations

• G.m = sSup ((fun (M : G.Subgraph) => ↑M.edgeSet.toFinset.card) '' {M : G.Subgraph | M.IsMatching})

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

The maximum cardinality among all independent sets s that maximize the quantity |s| - |N(s)|, where N(s) is the neighborhood of the set s.

Equations

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

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

largestInducedForestSize G is the size of a largest induced forest of G.

Equations

• G.largestInducedForestSize = sSup {n : ℕ | ∃ (s : Finset α), (SimpleGraph.induce (↑s) G).IsAcyclic ∧ s.card = n}

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.largestInducedBipartiteSubgraphSize {α : Type u_1} (G : SimpleGraph α) : ℕ

largestInducedBipartiteSubgraphSize G is the size of a largest induced bipartite subgraph of G.

Equations

• G.largestInducedBipartiteSubgraphSize = sSup {n : ℕ | ∃ (s : Finset α), (SimpleGraph.induce (↑s) G).IsBipartite ∧ s.card = n}

noncomputable def SimpleGraph.b {α : Type u_1} (G : SimpleGraph α) : ℝ

b G is the number of vertices of a largest induced bipartite subgraph of G. Returned as a real number.

Equations

• G.b = ↑G.largestInducedBipartiteSubgraphSize

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

Independence number of the neighbourhood of v.

Equations

• G.indepNeighborsCard v = (SimpleGraph.induce (G.neighborSet v) G).indepNum

noncomputable def SimpleGraph.indepNeighbors {α : Type u_1} (G : SimpleGraph α) (v : α) : ℝ

The same quantity as a real number.

Equations

• G.indepNeighbors v = ↑(G.indepNeighborsCard v)

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

Average of indepNeighbors over all vertices.

Equations

• G.averageIndepNeighbors = (∑ v : α, G.indepNeighbors v) / ↑(Fintype.card α)

def SimpleGraph.UnitDistancePlaneGraph (V : Set (EuclideanSpace ℝ (Fin 2))) : SimpleGraph ↑V

A unit distance graph in ℝ²: A graph where the vertices V are a collection of points in ℝ² and there is an edge between two points if and only if the distance between them is 1.

Equations

• SimpleGraph.UnitDistancePlaneGraph V = { Adj := fun (x y : ↑V) => dist x y = 1, symm := ⋯, loopless := ⋯ }

def SimpleGraph.InternallyDisjoint {V : Type u_2} {G : SimpleGraph V} {u v x y : V} (p : G.Walk u v) (q : G.Walk x y) : Prop

Two walks are internally disjoint if they share no vertices other than their endpoints.

Equations

• SimpleGraph.InternallyDisjoint p q = p.support.tail.dropLast.Disjoint q.support.tail.dropLast

def SimpleGraph.InfinitelyConnected {V : Type u_2} (G : SimpleGraph V) : Prop

We say a graph is infinitely connected if any two vertices are connected by infinitely many pairwise disjoint paths.

Equations

• G.InfinitelyConnected = Pairwise fun (u v : V) => ∃ (P : Set (G.Walk u v)), P.Infinite ∧ (∀ p ∈ P, p.IsPath) ∧ P.Pairwise SimpleGraph.InternallyDisjoint

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 (resp. clique number) of a graph with unbounded degree (resp. clique size) 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

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

Equations

• G.ecliqueNum = ⨆ (s : Finset V), ⨆ (_ : G.IsClique ↑s), ↑s.card