Quasi-isometries

structure BranchingProcess.IsQIWith {V : Type u_1} {V' : Type u_2} (D : ℕ) (G : SimpleGraph V) (G' : SimpleGraph V') (f : V → V') : Prop

f is a D-quasi-isometry from G to G': all three constants equal to D, the lower bound carried in the subtraction-free form d ≤ D d' + D².

• upper (x y : V) : G'.dist (f x) (f y) ≤ D * G.dist x y + D
• lower (x y : V) : G.dist x y ≤ D * G'.dist (f x) (f y) + D * D
• dense (y' : V') : ∃ (x : V), G'.dist (f x) y' ≤ D

def BranchingProcess.QuasiIsometric {V : Type u_1} {V' : Type u_2} (G : SimpleGraph V) (G' : SimpleGraph V') : Prop

G and G' are quasi-isometric: some map is a D-quasi-isometry for some D.

Equations

• BranchingProcess.QuasiIsometric G G' = ∃ (D : ℕ) (f : V → V'), BranchingProcess.IsQIWith D G G' f

Betweenness

def BranchingProcess.Between {V : Type u_1} (G : SimpleGraph V) (u m v : V) : Prop

m lies between u and v: every walk from u to v meets m.

Equations

• BranchingProcess.Between G u m v = ∀ (p : G.Walk u v), m ∈ p.support

theorem BranchingProcess.between_left {V : Type u_1} (G : SimpleGraph V) (u v : V) : Between G u u v

The left endpoint lies between itself and any vertex.

theorem BranchingProcess.between_right {V : Type u_1} (G : SimpleGraph V) (u v : V) : Between G u v v

The right endpoint lies between any vertex and itself.

theorem BranchingProcess.Between.symm {V : Type u_1} {G : SimpleGraph V} {u m v : V} (h : Between G u m v) : Between G v m u

Betweenness is symmetric in its outer arguments.

theorem BranchingProcess.Between.dist_add {V : Type u_1} {G : SimpleGraph V} (hG : G.Connected) {u m v : V} (h : Between G u m v) : G.dist u m + G.dist m v = G.dist u v

A vertex between two others splits the distance.

theorem BranchingProcess.between_of_mem_support {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) {u v m : V} {p : G.Walk u v} (hp : p.IsPath) (hm : m ∈ p.support) : Between G u m v

In a tree a vertex on one path from u to v lies on every walk from u to v: the unique path is a bypass of every walk.

theorem BranchingProcess.between_iff_dist_add {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) {u m v : V} : Between G u m v ↔ G.dist u m + G.dist m v = G.dist u v

In a tree, betweenness is the additivity of the distance.

theorem BranchingProcess.between_or {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) {u m w : V} (h : Between G u m w) (v : V) : Between G u m v ∨ Between G v m w

In a tree, a vertex separating u from w separates u from v or v from w: the concatenation of the two paths through v is a walk from u to w.

Stability of quasi-geodesics in a tree

theorem BranchingProcess.exists_between_dist_le {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (hG' : G'.IsTree) {D : ℕ} {f : V → V'} (hf : IsQIWith D G G' f) {x y : V} (p : G.Walk x y) {m : V'} (hm : Between G' (f x) m (f y)) : ∃ i ≤ p.length, G'.dist (f (p.getVert i)) m ≤ D

Stability. Let f be a D-quasi-isometry into a tree and let m separate f x from f y. Then some vertex of any walk from x to y has its image within D of m. Consecutive vertices of the walk have images at distance at most 2D, and a consecutive pair straddling m would be at distance more than 2D if both were more than D from m.

Rays and lines

def BranchingProcess.IsRay {V : Type u_1} (G : SimpleGraph V) (r : ℕ → V) : Prop

A ray: a map ℕ → V isometric onto its image.

Equations

• BranchingProcess.IsRay G r = ∀ (m n : ℕ), G.dist (r m) (r n) = m.dist n

def BranchingProcess.IsLine {V : Type u_1} (G : SimpleGraph V) (l : ℤ → V) : Prop

A line: a map ℤ → V isometric onto its image.

Equations

• BranchingProcess.IsLine G l = ∀ (m n : ℤ), G.dist (l m) (l n) = (m - n).natAbs

theorem BranchingProcess.natDist_eq_natAbs (m n : ℕ) : m.dist n = (↑m - ↑n).natAbs

The natural distance as the absolute value of the integer difference.

theorem BranchingProcess.IsLine.isRay_right {V : Type u_1} {G : SimpleGraph V} {l : ℤ → V} (hl : IsLine G l) (k : ℤ) : IsRay G fun (n : ℕ) => l (k + ↑n)

The half-line of a line to the right of a parameter is a ray.

theorem BranchingProcess.IsLine.isRay_left {V : Type u_1} {G : SimpleGraph V} {l : ℤ → V} (hl : IsLine G l) (k : ℤ) : IsRay G fun (n : ℕ) => l (k - ↑n)

The half-line of a line to the left of a parameter is a ray.

theorem BranchingProcess.IsLine.adj {V : Type u_1} {G : SimpleGraph V} {l : ℤ → V} (hl : IsLine G l) (k : ℤ) : G.Adj (l k) (l (k + 1))

Consecutive vertices of a line are adjacent.

theorem BranchingProcess.IsLine.ne {V : Type u_1} {G : SimpleGraph V} {l : ℤ → V} (hl : IsLine G l) (k : ℤ) : l (k + 1) ≠ l (k - 1)

A line leaves a vertex through two distinct neighbours.

theorem BranchingProcess.IsLine.exists_far {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) {l : ℤ → V} (hl : IsLine G l) (k : ℤ) (w : V) (n : ℕ) : ∃ (z : V), G.dist (l k) z = n ∧ Between G w (l k) z

The two half-rays. Given a vertex w and a parameter k on a line of a tree, one of the two half-rays at l k runs away from w through l k: it carries, at each distance n, a vertex z with l k between w and z.

Hairs

def BranchingProcess.IsHair {V : Type u_1} (G : SimpleGraph V) (c : V) (P : Set V) (h : ℕ) : Prop

P is a hair of depth h at c: a connected component of the complement of {c}, contained in the ball of radius h around c and meeting its boundary.

Equations

• BranchingProcess.IsHair G c P h = ((∃ (C : G.ComponentCompl {c}), ↑C = P) ∧ (∀ v ∈ P, G.dist v c ≤ h) ∧ ∃ v ∈ P, G.dist v c = h)

theorem BranchingProcess.mem_componentCompl_of_walk {V : Type u_1} {G : SimpleGraph V} {c : V} {C : G.ComponentCompl {c}} {a b : V} (W : G.Walk a b) : c ∉ W.support → b ∈ C → a ∈ C

A walk missing c and ending in a component of the complement of {c} starts in that component.

theorem BranchingProcess.between_of_notMem_componentCompl {V : Type u_1} {G : SimpleGraph V} {c : V} {C : G.ComponentCompl {c}} {x q : V} (hx : x ∈ C) (hq : q ∉ C) : Between G q c x

The separation by a hair. A vertex outside a component of the complement of {c} is separated from every vertex of that component by c.

Hairs against lines

theorem BranchingProcess.not_quasiIsometric_of_hair_of_line {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} {R : ℕ} (hG : G.IsTree) (hG' : G'.IsTree) (hhair : ∀ (n : ℕ), ∃ (c : V) (P : Set V) (h : ℕ), n < h ∧ IsHair G c P h) (hline : ∀ (u : V'), ∃ (l : ℤ → V') (k : ℤ), IsLine G' l ∧ G'.dist u (l k) ≤ R) : ¬QuasiIsometric G G'

The hair separation. A tree with hairs of unbounded depth is not quasi-isometric to a tree all of whose vertices lie within a bounded distance of a line.

The ray

def BranchingProcess.rayGraph : SimpleGraph ℕ

The ray: ℕ with the path-graph structure.

Equations

• BranchingProcess.rayGraph = { Adj := fun (m n : ℕ) => m + 1 = n ∨ n + 1 = m, symm := BranchingProcess.rayGraph._proof_3, loopless := BranchingProcess.rayGraph._proof_4 }

@[simp]

theorem BranchingProcess.rayGraph_adj {m n : ℕ} : rayGraph.Adj m n ↔ m + 1 = n ∨ n + 1 = m

Adjacency in the ray: the two vertices differ by one.

def BranchingProcess.rayUp (a k : ℕ) : rayGraph.Walk a (a + k)

The walk climbing k steps from a.

Equations

• BranchingProcess.rayUp a 0 = SimpleGraph.Walk.nil
• BranchingProcess.rayUp a k.succ = (BranchingProcess.rayUp a k).concat ⋯

@[simp]

theorem BranchingProcess.rayUp_length (a k : ℕ) : (rayUp a k).length = k

The climbing walk has the expected length.

theorem BranchingProcess.rayGraph_reachable (a b : ℕ) : rayGraph.Reachable a b

The ray is connected: climbing joins any two vertices.

theorem BranchingProcess.rayGraph_dist_le (a b : ℕ) : rayGraph.dist a b ≤ a.dist b

The climbing walk bounds the graph metric of the ray.

theorem BranchingProcess.rayGraph_le_length {a b : ℕ} (W : rayGraph.Walk a b) : a.dist b ≤ W.length

Each step of a walk in the ray moves the parameter by one, so the natural distance bounds the length.

theorem BranchingProcess.rayGraph_dist (a b : ℕ) : rayGraph.dist a b = a.dist b

The graph metric of the ray is the natural distance.

theorem BranchingProcess.rayGraph_connected : rayGraph.Connected

The ray is connected.

theorem BranchingProcess.rayGraph_isAcyclic : rayGraph.IsAcyclic

The ray is acyclic: deleting an edge separates the vertices below it from those above.

theorem BranchingProcess.rayGraph_isTree : rayGraph.IsTree

The ray is a tree.

Three rays against the ray

theorem BranchingProcess.IsRay.eq_of_between {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) {r : ℕ → V} (hr : IsRay G r) {n : ℕ} {u : V} (hu : Between G (r 0) u (r n)) : u = r (G.dist (r 0) u)

A geodesic out of the initial vertex of a ray runs along the ray: a vertex between r 0 and r n is the vertex of the ray at its own distance from r 0.

theorem BranchingProcess.dist_ray_branch {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) {r s : ℕ → V} (hr : IsRay G r) (hs : IsRay G s) (h0 : r 0 = s 0) (hmeet : ∀ (m n : ℕ), r m = s n → r m = r 0) (m n : ℕ) : G.dist (r m) (s n) = m + n

Two rays branch. Two rays of a tree leaving a common initial vertex and meeting only there are at distance the sum of the parameters.

theorem BranchingProcess.not_quasiIsometric_rayGraph {V : Type u_1} {G : SimpleGraph V} (hG : G.IsTree) {v : V} {ray : Fin 3 → ℕ → V} (hray : ∀ (i : Fin 3), IsRay G (ray i)) (hbase : ∀ (i : Fin 3), ray i 0 = v) (hmeet : ∀ (i j : Fin 3), i ≠ j → ∀ (m n : ℕ), ray i m = ray j n → ray i m = v) : ¬QuasiIsometric G rayGraph

The three-rays obstruction. A tree carrying three rays that pairwise meet only in their common initial vertex is not quasi-isometric to the ray.