Random regular graphs are optimal expanders

Stream: graph theory

[Laura Monk]

Hi! I have been setting up a project aiming to prove Alon's conjecture / Friedman's theorem, namely that random regular graphs are near-optimal expanders. This is an influential result in spectral graph theory which was historically very difficult to prove, but a new very clean and short proof has recently emerged.

Interestingly, the proof I want to use relies on random graphs obtained from random permutations, and will have some loops and multi-edges. This project therefore requires to develop Graph, and I hope it can be a motivation to do so. I am not very experienced in Lean and I would be very happy to welcome people to the project; there is a lot to do, with very different types of maths / level of challenge I think. I also highlighted a few side-projects I think would be interesting in the blueprint.

Links: the github repo

[Fred Rajasekaran]

This looks interesting! Will you need to develop all of the random matrix theory/free probability used in the paper? I don't think any of this is in mathlib yet. I have some very basic random matrix theory lemmas and am working on some moment method arguments on a project on the Semicircle Law (github). It's still a work in progress but some of it might be of use. I introduced something called a LoopWalk which is basically a walk on a simple graph that allows for loops at a vertex (it doesn't have multiple edges yet). I avoided using Graph since it was pretty underdeveloped when I started, but this might be a time to build it up.

[Laura Monk]

Thank you for your interest! The survey goes far, far beyond what we need to prove Friedman's theorem so we will focus on what we need (which is also why I picked this goal). I have been chatting with the author and quite a few things can be stripped for this. However you are right I am not quite sure how to deal with probabilities!

[Laura Monk]

Your project on the semicircle law is probably going to be good inspiration since a natural subproject here is to prove weak convergence to the Kesten law.

[David Ledvinka]

I'd definitely be happy to help with this! Especially the probability aspects!

[Laura Monk]

Amazing! Would you like to think about how to define the random graphs? The definition I had in mind is in the blueprint but I am not sure yet how exactly it works to "take k iid permutations uniformly" in Lean.

[David Ledvinka]

As a rough draft something like this works I think:

import Mathlib

variable {𝓧 𝓨 𝓩 : Type*} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {m𝓩 : MeasurableSpace 𝓩}

-- Missing from mathlib
instance : MeasurableSpace (Equiv 𝓧 𝓨) := sorry
instance : MeasurableSpace (Matrix 𝓧 𝓨 𝓩) := sorry

open MeasureTheory ProbabilityTheory Measure

variable (V ι : Type*) [Fintype V] [Fintype ι] {mV : MeasurableSpace V}

noncomputable def iid_uniform_permutations_measure :
    Measure (ι → Equiv.Perm V) :=
  Measure.pi (fun _ ↦ uniformOn .univ)

open Classical in
noncomputable def random_graph_adjacency_matrix_measure :
    Measure (Matrix V V ℕ) :=
  (iid_uniform_permutations_measure V ι).map (fun σ ↦ ∑ i ∈ .univ, ((σ i).permMatrix ℕ + ((σ i).permMatrix ℕ).transpose))

From here you can map it to a measure on graphs by a map from the adjacency matrices to graphs (I am not familiar with the graph theory library yet though). Exactly how you do it probably depends on what will make the arguments convenient . In particular if all the probabilitistic arguments takes place in the random matrix setting (and all the graph theory arguments are deterministic arguments) then you would prefer something that works nice for doing random matrix theory (and even within random matrix theory the nature of the arguments will effect what works best I think).

[Snir Broshi]

I'm not sure about this, but shouldn't there be a docs#ProbabilityTheory.iIndepFun somewhere to express independence?

[David Ledvinka]

I constructed the measure as a product. There are no random variables involved. If you take any sequence of i.i.d random uniform permutations (so functions of type ι → Ω → Equiv.Perm V) their pushforward measure (as a function Ω → ι → Equiv.Perm V) should be iid_uniform_permutations_measure.

[David Ledvinka]

For some arguments you would prefer a random variable perspective and for some arguments you would prefer a measure perspective. In paper math we often switch between the two perspective without saying a word (there is a bunch of invisible math here).

[Laura Monk]

Thank you! I will try and build the graph from this next week then :)