Summing over Fin n

Stream: Is there code for X?

[Swarnava Chakraborty]

My exact goal is

(∑ x, if G.Edges[↑x] = s(i, j) then -1 else 0) = SimpleGraph.lapMatrix ℚ G i j

with the definition

noncomputable def Edges (G : SimpleGraph V) [DecidableRel G.Adj] : List (Sym2 V) :=
  List.filter (fun e => e ∈ G.edgeSet) (Finset.sym2 Finset.univ).toList

I found a theorem Finset.sum_ite_eq but that is for summing over Finsets, but by x in the above goal is in Fin G.Edges.length. Can anyone give me any way for this?

[Aaron Liu]

The finset sum lemma should probably work, since this is secretly a sum over Finset.univ.

[Swarnava Chakraborty]

I do not think this is working in my case. Could you just give an example on how to use it?

[Aaron Liu]

Can you give a #mwe?

[Matt Diamond]

@Swarnava Chakraborty if you can find a way to rewrite the left-hand side to this:

∑ x ∈ G.Edges.toFinset, if x = s(i, j) then -1 else 0

(which I believe is equivalent to your original statement) then you should be able to rewrite that with Finset.sum_ite_eq'

it may be simpler to define Edges to return a Finset instead of a List, allowing you to sum over it without needing the .toFinset call

[Yury G. Kudryashov]

Yes, going from Finset to List and back again seems unnecessary.

[Swarnava Chakraborty]

Thanks for the suggestions , but at this point I have used so many properties of lists at so many places for Edges that it would be real pain to redefine it. I will try out converting to Finset