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.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 α)

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

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

theorem SimpleGraph.indep_num_eq_computable {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] : G.indepNum = G.computable_indep_num

Equivalence between computable and noncomputable independence number.

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

Maximum local independence number over all vertices. For each vertex, we compute the independence number of the subgraph induced by its neighbors, and take the maximum over all vertices.

Equations

• G.maxLocalIndependence = Option.getD (Finset.image (fun (v : α) => (SimpleGraph.induce (G.neighborSet v) G).indepNum) Finset.univ).max 0

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

Minimum local independence number over all vertices. For each vertex, we compute the independence number of the subgraph induced by its neighbors, and take the minimum over all vertices.

Equations

• G.minLocalIndependence = Option.getD (Finset.image (fun (v : α) => (SimpleGraph.induce (G.neighborSet v) G).indepNum) Finset.univ).min 0