## 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?

#### Gabriel Moise (Jul 11 2021 at 09:02):

Gabriel Moise said:

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 (Jul 11 2021 at 15:56):

@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 (Jul 11 2021 at 23:01):

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 (Jul 12 2021 at 05:00):

Gabriel Moise said:

Gabriel Moise said:

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 (Jul 12 2021 at 05:01):

I too am reviewing it now.

#### Kyle Miller (Jul 12 2021 at 05:04):

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

#### Kyle Miller (Jul 12 2021 at 18:21):

@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 (Jul 12 2021 at 18:38):

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

#### Kyle Miller (Jul 12 2021 at 18:47):

@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 (Jul 12 2021 at 20:09):

@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 (Jul 12 2021 at 21:30):

@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 (Jul 14 2021 at 05:31):

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

Last updated: Dec 20 2023 at 11:08 UTC