Walk on SimpleGraph, Consecutive Visits to Vertex Allowed

Stream: Is there code for X?

[Fred Rajasekaran]

Is there an easy way to handle walks on a simple graph but allow consecutive visits to the same vertex and have them contribute to the length of the walk? And will I need to define a new inductive type or is there a way to build it on top of the way walks are already defined?

For example if $X$ is an $n \times n$ matrix and $p \geq 2$ an integer, I want to enumerate the sum on the RHS of

$$\mathrm{Tr}[X^p] = \sum_{1 \leq i_1, \dots, i_p \leq n}X_{i_1 i_2} X_{i_2 i_3} \dots X_{i_p i_1}$$

by closed walks of length $p$ on the complete graph on $n$ vertices, but I need to allow loops in order to include entries of the form $X_{ii}$ in the sum. I'd like to do this within the SimpleGraph structure since I'll need to change the type of graphs/walks I'm summing over throughout a proof and SimpleGraph seems to have the most API out of all the graphs in lean. I will also eventually rule out having any loops so I will end up with a walk on a simple graph as defined in Combinatorics/SimpleGraph/Walk.lean anyway.

[Shreyas Srinivas]

Doesn’t docs#SimpleGraph.Walk already do this?

[Shreyas Srinivas]

Oh you want to loop at the same vertex?

[Shreyas Srinivas]

I don’t think there is such a structure yet. Most likely because it doesn’t make sense for SimpleGraphs because they are loopless

[Laura Monk]

There is now a graph structure which allows for loops so that would be a way, but this is very recent and there is none of the useful tools from simplegraphs yet. I might work on bringing some of these there as I need them for graphs with loops and multiedges myself.