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.edist w u < G.edist 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

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

theorem SimpleGraph.szeged_eq_computable {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] : G.szegedIndex = G.computable_szeged_index