The total non-backtracking walk count

This file defines nbTotalWalks — mₖ, the total number of length-k non-backtracking walks in a graph, summed over all ordered start/end vertex pairs. This is the quantity fed to the Alon–Hoory–Linial irregular Moore bound chain; the walk-count and average-degree lemmas that consume it live downstream (AHL.AHLAmGm, Band.Sum).

def ACMax.nbTotalWalks {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) : ℕ

mₖ: the total number of length-k non-backtracking walks, summed over all ordered start/end pairs. By definition this is ∑ x, ∑ v, ((G.finsetWalkLength k x v).filter …).card.

Equations

• ACMax.nbTotalWalks G k = ∑ x : V, ∑ v : V, (Finset.filter ACMax.IsNonBacktracking (G.finsetWalkLength k x v)).card