noncomputable def Matrix.IsHermitian.maxEigenvalue {𝕜 : Type u_1} [Field 𝕜] [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : ℝ

Equations

• hA.maxEigenvalue = iSup hA.eigenvalues

@[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

• G.ecc S = if h : {v : α | v ∉ S}.Nonempty then (Finset.image (fun (v : α) => G.distToSet v S) {v : α | v ∉ S}).max' ⋯ else 0

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

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

The Wiener index of G, which is the sum of distances between all pairs of vertices.

Equations

• G.wienerIndex = ∑ uv : Sym2 α, Sym2.lift ⟨fun (u v : α) => G.dist u v, ⋯⟩ uv

noncomputable def SimpleGraph.szeged_aux {α : Type u_1} [Fintype α] (G : SimpleGraph α) (u v : α) : ℕ

Auxiliary function for Szeged index: counts vertices closer to u than v.

Equations

• G.szeged_aux u v = {w : α | G.dist w u ≠ 0 ∧ G.dist w u ≤ G.dist w v}.card

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

The Szeged index of G.

This is define as the sum ∑_{uv ∈ E(G)} n_u(u,v) * n_v(u,v) where n_u(uv) is the number of vertices closer to u than v.

Equations

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

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

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

The annihilation number of a graph. This is the largest number of degrees that can be added together without going over the total number of edges of that graph.

Equations

• G.annihilationNumber = {S ∈ Finset.Iic G.degreeMultiset | S.sum ≤ G.edgeFinset.card}.sup Multiset.card

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

Computes the annihilation number of a graph G.

It calculates the degree sequence, sorts it ascendingly, and finds the largest prefix length 'k' (where 0 ≤ k ≤ |V(G)|) such that the sum of the prefix is less than or equal to the sum of the corresponding suffix.

Equations

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

Residue

The residue of a graph is the number of zeros remaining after iteratively applying the Havel-Hakimi algorithm to the degree sequence until all remaining degrees are zero.

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

Computes the residue of a graph G, ,i.e. the number of zeros remaining after iteratively applying the Havel-Hakimi algorithm to the degree sequence until all remaining degrees are zero. Starts with the descending degree sequence and applies the Havel-Hakimi process.

Equations

• G.residue = SimpleGraph.residueAux✝ (Finset.sort (fun (x1 x2 : ℕ) => x1 ≥ x2) (Finset.image (fun (v : α) => G.degree v) Finset.univ))

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

Fractional alpha. This is defined as $$ \max_x \sum_{v \in V} x_v $$ subject to $0 \le x_v \le 1$ for all $v \in V$ and $x_u + x_v \le 1$ whenever $(u, v)$ are connected by an edge.

Equations

• G.fractionalAlpha = sSup {x : ℝ | ∃ (x_1 : α → ℝ) (_ : ∀ (v : α), x_1 v ∈ Set.Icc 0 1) (_ : ∀ (u v : α), G.Adj u v → x_1 u + x_1 v ≤ 1), ∑ i : α, x_1 i = x}

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

Lovász Theta Function (ϑ(G)) The Lovász theta function is defined as: ϑ(G) = min λ_max(A) where the minimum is taken over all symmetric matrices A such that:

A_ij = 1 for all i = j (diagonal entries are 1) A_ij = 0 for all {i,j} ∈ E (entries corresponding to edges are 0) A is positive semidefinite

Here λ_max(A) denotes the maximum eigenvalue of A.

Equations

• G.lovaczThetaFunction = sInf {x : ℝ | ∃ (A : Matrix α α ℝ) (hA : A.IsHermitian) (_ : ∀ (i : α), A i i = 1) (_ : ∀ (i j : α), G.Adj i j → A i j = 0), hA.maxEigenvalue = x}

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

Given a simple graph G with adjacency matrix A, this is the number n₀ + min n₊ n₋ where:

• n₀ is the multiplicity of zero as an eigenvalue of A
• n₊ is the number of positive eigenvalues of A (counting multiplicities)
• n₋ is the number of negative eigenvalues of A (counting multiplicities)

Equations

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