Spectrum of a graph

Stream: graph theory

[Gabriel Moise]

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]

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]

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]

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]

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]

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]

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]

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

[Eric Wieser]

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

[Gabriel Moise]

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

[Eric Wieser]

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

[Gabriel Moise]

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]

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]

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]

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]

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

[Gabriel Moise]

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

[Eric Wieser]

Oh, that wasn't clear

[Gabriel Moise]

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]

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

[Gabriel Moise]

Made the PR, https://github.com/leanprover-community/mathlib/pull/7498

[Gabriel Moise]

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]

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]

You can condition on [inhabited V]

[Eric Wieser]

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

[Aaron Anderson]

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]

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]

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]

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

@[ext]
structure orientation (G : simple_graph V) :=
(head : G.edge_set → 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]

That goal looks true to me

[Eric Wieser]

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

[Eric Wieser]

It's docs#quotient.out_eq

[Eric Wieser]

Maybe try using quotient.out instead?

[Gabriel Moise]

Gabriel Moise said:

Made the PR, https://github.com/leanprover-community/mathlib/pull/7498

Hey!
Seems like the PR has been idle for some time. Are there any other suggestions to be made, or any work in progress for it? :smile:

[Kyle Miller]

@Gabriel Moise I'm happy to see PRs on the way toward graph Laplacians!

For orientations, I'm wondering if it would be better dealing with directed graphs instead. It also might make sense if this were all for multigraphs rather than simple graphs. The code for orientations could probably be used (with modification) to turn undirected graphs into directed graphs.

I'll try putting together a PR for directed graphs and multigraphs today

[Kyle Miller]

Here's a branch with a definition of multigraphs https://github.com/leanprover-community/mathlib/tree/multigraphs/src/combinatorics/multigraph

There's a multigraph.to_multidigraph function that chooses arbitrary edge orientations.

I didn't get around to finite multigraphs yet, other than local finiteness to be able to define degree.

[Johan Commelin]

Gabriel Moise said:

Gabriel Moise said:

Made the PR, https://github.com/leanprover-community/mathlib/pull/7498

Hey!
Seems like the PR has been idle for some time. Are there any other suggestions to be made, or any work in progress for it? :smile:

@Kyle Miller @Alena Gusakov @Bhavik Mehta I think you're best at reviewing these PRs. Let me know if you want my input.

[Yaël Dillies]

I too am reviewing it now.

[Kyle Miller]

(Speaking of which, I've contributed too much to #8223 to review it, I think. This is homomorphisms and subgraphs.)

[Kyle Miller]

@Johan Commelin The usual definition of an incidence matrix $I$ is a $n\times m$ matrix where $n$ is the number of vertices and $m$ is the number of edges. This is easy enough to work with for mathematicians who are good at coercing stuff without blinking. But there's a possibility to redefine it so that the columns correspond to the set of all unordered pairs, setting all the irrelevant columns to $0$, saving a whole lot of coercions at the cost of being conceptually a bit different. This does not affect what $II^T$ is, which seems to be the important thing.

Do you have any thoughts about using the "junk data principle" here?

[Yaël Dillies]

Oooh I didn't catch it, but #7498 is defining the adjacency matrix, not the incidence matrix!

[Kyle Miller]

@Yaël Dillies The adjacency matrix would be adj_matrix : matrix V V R (see docs#simple_graph.adj_matrix), but this is inc_matrix : matrix V G.edge_set R, unless I'm missing something

[Johan Commelin]

@Kyle Miller hmm, I don't have a very good intuition here. But if you think including junk makes your life easier, well, go for it :smiley:

[Kyle Miller]

@Johan Commelin It seems to simplify things a good amount (50% less code for unoriented incidence matrices) https://gist.github.com/kmill/7f876df1d581047cd8dc56ffafa291d0

The theorems can also all be put together into a single statement (this is using the fact that the extra columns are 0, so it's not exactly junk data):

theorem inc_matrix_mul_transpose :
  G.inc_matrix R ⬝ (G.inc_matrix R)ᵀ = λ i j,
    if i = j then G.degree i else if G.adj i j then 1 else 0

I think @Gabriel Moise would prefer that incidence matrices more accurately reflect the definition you find in mathematics, but this break with tradition seems reasonably-well justified to me.

[Yaël Dillies]

Kyle Miller said:

Yaël Dillies The adjacency matrix would be adj_matrix : matrix V V R (see docs#simple_graph.adj_matrix), but this is inc_matrix : matrix V G.edge_set R, unless I'm missing something

Whoops don't mind me