Eigenvalues of SRGs

Stream: new members

[Rida Hamadani]

A lot of research in strongly regular graphs (docs#IsSRGWith) uses the following fact:
The eigenvalues of an IsSRGWith n k ℓ μ are k, r, and s, where:

$$r, s = \frac{\lambda - \mu \pm \sqrt{\left(\lambda-\mu\right)^2 + 4\left(k - \mu\right)}}{2}$$

and their respective multiplicities are 1, f, g, where:

$$f, g = \frac{1}{2}\left(n-1\mp\frac{2k+\left(n-1\right)\left(\lambda-\mu\right)}{ \sqrt{\left(\lambda-\mu\right)^2 + 4\left(k - \mu\right)}} \right)$$

What is the best way to state this in lean? You can find a proof of this fact at page 13 here. My problem is that there seems to be many different definitions of eigenvalues in mathlib. In particular, we need to be able to use the spectral_theorem in the proof. I would like to use the definitions in this file, but I do not understand how it works, for instance, what is "the index type" of a matrix, how do I differentiate which eigenvector is which, how can I apply a lemma from Module.End (for example docs#Module.End.mem_eigenspace_iff) on these values?

Apologies if this question is poorly worded, but I don't know how to provide an #mwe because I'm confused about how to even state the lemma. For context, 2 months ago I've tried proving a special case of the lemma mentioned above (here) and I kind of gave up on it due to how confusing proving stuff with eigenvalues was.

[Yaël Dillies]

Answering a bit of your question: docs#SimpleGraph.adjMatrix is a matrix with "index type" the vertex set of the simple graph

[Rida Hamadani]

My intuition is that indexing requires an ordering, is that not true?

[Yaël Dillies]

It is indeed not true