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

The independence number of a graph G.

Equations

• G.a = ↑G.indepNum

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

f G is the number of vertices of a largest induced forest of G as a real.

Equations

• G.f = ↑G.largestInducedForestSize

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