# Zulip Chat Archive

## 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 04 2021 at 17:44):

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

#### 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) :=
(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 (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:57):

It's docs#quotient.out_eq

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

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 (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:

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 (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: Aug 03 2023 at 10:10 UTC