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. Note that graphs with at most one vertex are not classed as infinitely connected.

Equations

• G.InfinitelyConnected = (Nontrivial V ∧ 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

def SimpleGraph.bfs_expand {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (S : Finset α) : Finset α

BFS expansion: add all neighbors of S to S.

Equations

• G.bfs_expand S = S ∪ S.biUnion fun (v : α) => Finset.filter (G.Adj v) Finset.univ

def SimpleGraph.bfs_dist_aux {α : Type u_1} [DecidableEq α] [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] (target : α) : ℕ → ℕ → Finset α → ℕ

Equations

• G.bfs_dist_aux target 0 x✝¹ x✝ = 0
• G.bfs_dist_aux target fuel.succ x✝¹ x✝ = if target ∈ x✝ then x✝¹ else G.bfs_dist_aux target fuel (x✝¹ + 1) (G.bfs_expand x✝)

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

Computable graph distance via BFS. Returns 0 if u = v or if v is unreachable from u.

Equations

• G.computable_dist u v = if u = v then 0 else G.bfs_dist_aux v (Fintype.card α) 1 (G.bfs_expand {u})

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

Computable independence number via powerset enumeration.

Equations

• G.computable_indep_num = {s ∈ Finset.univ.powerset | ∀ u ∈ s, ∀ v ∈ s, u ≠ v → ¬G.Adj u v}.sup Finset.card

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

Computable domination number via powerset enumeration.

Equations

• G.computable_dom_num = {D ∈ Finset.univ.powerset | ∀ (v : α), v ∈ D ∨ ∃ w ∈ D, G.Adj v w}.inf' ⋯ Finset.card

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

Computable Wiener index: half the sum of all ordered pairwise distances.

Equations

• G.computable_wiener = (∑ u : α, ∑ v : α, G.computable_dist u v) / 2

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

Computable average distance as a rational.

Equations

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

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

Computable Szeged auxiliary: count vertices closer to u than v.

Equations

• G.computable_szeged_aux u v = {w : α | G.computable_dist w u < G.computable_dist w v}.card

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

Computable Szeged index.

Equations

• G.computable_szeged_index = ∑ e ∈ G.edgeFinset, Sym2.lift ⟨fun (u v : α) => G.computable_szeged_aux u v * G.computable_szeged_aux v u, ⋯⟩ e