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

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

theorem SimpleGraph.wiener_eq_computable {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] : G.wienerIndex = G.computable_wiener