## Stream: graph theory

### Topic: Spectrum of a graph

#### Gabriel Moise (Apr 06 2021 at 08:29):

Hello! Is there a helpful library for showing stuff about eigenvalues of the matrices that could help me? I saw that the eigenspace.lean file has some lemmas, but what I have right now is this:

def has_eigen (M : matrix V V R) (μ : R) (x : V → R) : Prop :=
x ≠ 0 ∧ (mul_vec M x = μ • x)
def has_eigenvector (M : matrix V V R) (x : V → R) : Prop :=
∃ μ : R, has_eigen M μ x
def has_eigenvalue (M : matrix V V R) (μ : R) : Prop :=
∃ x : V → R, has_eigen M μ x


(a definition of eigenvalue+eigenvector in terms of matrices on a commutative ring R)

def symmetric_matrix (M : matrix V V R) : Prop := M = Mᵀ

def psd_matrix (M : matrix V V R) : Prop :=
symmetric_matrix M ∧ ∀ x : V → R, dot_product (vec_mul x M) x ≥ 0


(definitions of symmetry and positive semidefiniteness)

lemma psd_nonneg_eigenvalues {M : matrix V V R} (H_psd : psd_matrix M) (μ : R) (H : has_eigenvalue M μ) :
μ ≥ 0 := sorry


(I managed to prove that all eigenvalues of a PSD matrix are non-negative)

def laplace_matrix : matrix V V ℝ
| i j := if i = j then G.degree i else - G.adj_matrix ℝ i j


(the Laplacian matrix of a given undirected graph, with coefficients in ℝ)

lemma psd_laplacian (o : orientation G) : psd_matrix G.laplace_matrix := sorry
def laplacian_eigenvalues : set ℝ := {μ : ℝ | has_eigenvalue G.laplace_matrix μ}


(I managed to prove that the Laplacian of a graph is positive semi-definite and I defined it's set of eigenvalues)
Now, I easily have that the eigenvalues of the Laplacian are non-negative, but what I will want to work with after that is with l1,l2,...,ln where n is the number of vertices and li are the eigenvalues of the Laplacian. First, I need to show that the size of "laplacian_eigenvalues" is the size of V, basically to show that an n x n matrix that is positive semi-definite has n real eigenvalues, and since the smallest eigenvalue here is l1 = 0 (with corresponding eigenvector 1), I will want to work with l2 and ln. Also, I will probably need to work with the characteristic polynomial of a matrix.
I know this is a lot of information all over the place, if more clarification is needed, I will offer it. I just want some guidance on what libraries you think might be useful for me to progress, since I didn't find much in the "linear_algebra" file so far. Thank you very much!

#### Bryan Gin-ge Chen (Apr 06 2021 at 14:09):

I don't think we have anything on eigenvalues or eigenvectors outside of linear_algebra/eigenspace.lean. I encourage you to begin PR-ing what you have in "easily-reviewable" chunks, as the results you're proving seem quite valuable!

#### Gabriel Moise (Apr 06 2021 at 14:12):

Yes, will do. I will probably need some assistance with the PR process at start, but as soon as I have something more concrete I will PR it. This post was just to raise awareness and maybe someone more experienced has some guidance :smile:

#### Alena Gusakov (Apr 06 2021 at 16:32):

For l1, l2, ..., ln I think you could try list.sort? That's what I was messing around with when I was trying to prove Havel-Hakimi not too long ago

#### Gabriel Moise (May 03 2021 at 10:09):

Hello again! I came back to let you know that I kinda finished with some work on incidence and Laplacian matrices of graphs in the incidence.lean and laplacian.lean files from my repo : https://github.com/gabrielmoise/Lean-work (I also have a file with linear algebra, but that is for some future ideas regarding the spectrum of graphs).
I will probably want to PR most of the stuff there, but since I am not very experienced with Lean, I wanted to ask (if you can spare some minutes) if any of the more experienced in graph theory (and in Lean) people can have a look on what I did, some feedback would help a lot. Wish you a wonderful day! :smile:

#### Kevin Buzzard (May 03 2021 at 22:57):

lemma sum_complex_re {x : n → ℂ} : (∑ i : n, x i).re = ∑ i : n, (x i).re := by exact complex.re_lm.map_sum


lemma blah := by exact foo can just be shortened to lemma blah := foo -- by means "move from term mode to tactic mode" and exact means "move from tactic mode to term mode".

def vec_re (x : n → ℂ) : n → ℝ := λ i : n, (x i).re


You can move (i : n) before the colon and then you don't need the lambda in the proof. It doesn't change the type of vec_re. I mean def vec_re (x : n → ℂ) (i : n) : ℝ := (x i).re.

def Coe (M : matrix m n ℝ) := (M : matrix m n ℂ)


Every time you make a definition you need to make an API for that definition. This is just a coercion and we have an API for coercions already. Why make your life harder by making a new definition? Then you have to teach Lean how to use it.

In edge_val_equiv you could do rintro rfl instead of intro hyp, rw hyp.

dot_product_helper is surely never needed -- there are tactics like congr' which do it.

#### Gabriel Moise (May 04 2021 at 08:39):

The part with Coe was because it became annoying to write/read (M : matrix V V ℂ) in equations every time I needed to coerce M from reals to complex. I still don't know how to change this repetition.

#### Gabriel Moise (May 04 2021 at 08:42):

And for the rintro rfl part, for some reason the goal remains e₁.val = e₁.val.

#### Eric Wieser (May 04 2021 at 08:44):

A random tip: your degree_matrix is matrix.diagonal G.degree I think (docs#matrix.diagonal)

#### Gabriel Moise (May 04 2021 at 08:49):

It should do the trick, but types don't match right now, I will investigate

#### Eric Wieser (May 04 2021 at 08:56):

Maybe matrix.diagonal (λ v, G.degree v)

#### Gabriel Moise (May 04 2021 at 08:59):

Oh, and I notice now that in the incidence.lean file, what I created is not a directed incidence matrix, but an oriented incidence matrix for an oriented graph (not a directed graph). I am not sure how to rename it (I am not quite good with names) or_inc_matrix seems like it has something to do with the logical connective or. Any suggestions?

#### Eric Wieser (May 04 2021 at 09:09):

I'm not familiar with that terminology, but wikipedia tells me that oriented graphs are a subset of directed graphs, yet simple_graph is an undirected graph

#### Gabriel Moise (May 04 2021 at 09:10):

Yes, they are a subset of directed graphs, but they can be derived from an undirected graph by choosing an orientation on the edges.

#### Eric Wieser (May 04 2021 at 09:17):

Sure, but your definition doesn't say anything about that choice of orientation, so surely isn't about oriented graphs? (even if you can use it for them)

#### Eric Wieser (May 04 2021 at 09:18):

Remember the name is simple_graph.inc_matrix, which might already resolve whatever ambiguity you're seeing

#### Gabriel Moise (May 04 2021 at 09:19):

I was talking about the dir_inc_matrix I defined, which is dependent to the orientation o.

#### Eric Wieser (May 04 2021 at 09:19):

Oh, that wasn't clear

#### Gabriel Moise (May 04 2021 at 09:20):

Yes, I feel like I defined too many things in the incidence.lean file, so I will try to separate the new concepts I created into separate files. :smile: Sorry for the confusion!

#### Eric Wieser (May 04 2021 at 09:34):

The confusion was just in the wording of your zulip message!

#### Gabriel Moise (May 05 2021 at 18:54):

Apparently, one important thing I need to do is to provide my orientation structure with an inhabited instance. I am not sure I can do that, since I don't know how to retrieve any elements from a sym2 V. Does anyone have any ideas?

#### Kevin Buzzard (May 05 2021 at 18:57):

I've dealt with this in the past by giving it an explicit V, that seems to shut the linter up. But my impression is that people don't like this approach and would rather you just marked the definition with some kind of nolint or no_lint tag -- search for this in mathlib and you'll see examples

#### Eric Wieser (May 05 2021 at 19:10):

You can condition on [inhabited V]

#### Eric Wieser (May 05 2021 at 19:11):

And then you can get hold of a sym2 V with default (sym2 V)

#### Aaron Anderson (May 06 2021 at 02:14):

It sounds like what you need is to define an orientation on each individual sym2 edge using some kind of choice. For that, I see two options.

#### Aaron Anderson (May 06 2021 at 02:16):

sym2 is itself a quotient on V x V, so the most direct thing to try would be quot.out, which takes an element of a quotient and picks one of the possible elements of the equivalence class that corresponds to.

#### Aaron Anderson (May 06 2021 at 02:19):

The other option (a few more steps) is to use sym2.equiv_multiset to turn your sym2 into a multiset, because we have a more robust API for those. Then you can use for instance multiset.to_list to turn it into an ordered list, or show that there exists a member of the multiset using multiset.card_pos_iff_exists_mem and then use classical.some to pick one.

#### Gabriel Moise (May 06 2021 at 14:29):

With your idea with quot.out, I get stuck trying to prove the following:

@[ext]
structure orientation (G : simple_graph V) :=
(tail : G.edge_set → V)
(consistent (e : G.edge_set) : e.val = ⟦(head(e), tail(e))⟧)

noncomputable def default_orientation (G : simple_graph V) : orientation G :=
{
head := λ (e : G.edge_set), (quot.out (e : sym2 V)).fst,
tail := λ (e : G.edge_set), (quot.out (e : sym2 V)).snd,
consistent := λ (e : G.edge_set), begin rw prod.mk.eta, rw ←subtype.val_eq_coe, sorry end
-- e.val = ⟦quot.out e.val⟧
}

noncomputable instance (G : simple_graph V) : inhabited (orientation G) :=
⟨G.default_orientation⟩


Is what I am trying to prove even true?

#### Eric Wieser (May 06 2021 at 15:56):

That goal looks true to me

#### Eric Wieser (May 06 2021 at 15:56):

There'll be a lemma about docs#quot.out

#### Eric Wieser (May 06 2021 at 15:58):

Maybe try using quotient.out instead?

Last updated: May 08 2021 at 21:09 UTC