Grafting a leaf on a finite tree

The graph operation either adds a leaf at an existing branch vertex or subdivides an edge and attaches the new leaf to the subdivision vertex.

noncomputable def BGW.StableTrees.Marchal.graftGraph {m : ℕ} (G : SimpleGraph (Fin m)) (p : ↑G.edgeSet ⊕ { v : Fin m // 3 ≤ G.degree v }) : SimpleGraph (Fin (match p with | Sum.inl val => m + 2 | Sum.inr val => m + 1))

Graft a new leaf A_{n+1} (the last vertex) on the middle of an edge (new midpoint m, new leaf m+1) or on an internal vertex (new leaf m).

Equations

• One or more equations did not get rendered due to their size.

def BGW.StableTrees.Marchal.vertexNewLeaf (m : ℕ) : Fin (m + 1)

The new leaf in a vertex graft.

Equations

• BGW.StableTrees.Marchal.vertexNewLeaf m = ⟨m, ⋯⟩

def BGW.StableTrees.Marchal.vertexOld {m : ℕ} (x : Fin m) : Fin (m + 1)

Old vertices in a vertex graft.

Equations

• BGW.StableTrees.Marchal.vertexOld x = Fin.castAdd 1 x

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inr_adj_old_old {m : ℕ} (G : SimpleGraph (Fin m)) (v : { v : Fin m // 3 ≤ G.degree v }) (x y : Fin m) : (graftGraph G (Sum.inr v)).Adj (vertexOld x) (vertexOld y) ↔ G.Adj x y

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inr_adj_old_new {m : ℕ} (G : SimpleGraph (Fin m)) (v : { v : Fin m // 3 ≤ G.degree v }) (x : Fin m) : (graftGraph G (Sum.inr v)).Adj (vertexOld x) (vertexNewLeaf m) ↔ x = ↑v

theorem BGW.StableTrees.Marchal.graftGraph_inr_adj_new_new {m : ℕ} (G : SimpleGraph (Fin m)) (v : { v : Fin m // 3 ≤ G.degree v }) : ¬(graftGraph G (Sum.inr v)).Adj (vertexNewLeaf m) (vertexNewLeaf m)

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inr_adj_new_old {m : ℕ} (G : SimpleGraph (Fin m)) (v : { v : Fin m // 3 ≤ G.degree v }) (x : Fin m) : (graftGraph G (Sum.inr v)).Adj (vertexNewLeaf m) (vertexOld x) ↔ x = ↑v

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inr_degree_new {m : ℕ} (G : SimpleGraph (Fin m)) (v : { v : Fin m // 3 ≤ G.degree v }) : (graftGraph G (Sum.inr v)).degree (vertexNewLeaf m) = 1

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inr_degree_old_of_ne {m : ℕ} (G : SimpleGraph (Fin m)) (v : { v : Fin m // 3 ≤ G.degree v }) (x : Fin m) (hx : x ≠ ↑v) : (graftGraph G (Sum.inr v)).degree (vertexOld x) = G.degree x

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inr_degree_old_self {m : ℕ} (G : SimpleGraph (Fin m)) (v : { v : Fin m // 3 ≤ G.degree v }) : (graftGraph G (Sum.inr v)).degree (vertexOld ↑v) = G.degree ↑v + 1

def BGW.StableTrees.Marchal.edgeMidpoint (m : ℕ) : Fin (m + 2)

The subdivision midpoint in an edge graft.

Equations

• BGW.StableTrees.Marchal.edgeMidpoint m = ⟨m, ⋯⟩

def BGW.StableTrees.Marchal.edgeNewLeaf (m : ℕ) : Fin (m + 2)

The new leaf in an edge graft.

Equations

• BGW.StableTrees.Marchal.edgeNewLeaf m = ⟨m + 1, ⋯⟩

def BGW.StableTrees.Marchal.edgeOld {m : ℕ} (x : Fin m) : Fin (m + 2)

Old vertices in an edge graft.

Equations

• BGW.StableTrees.Marchal.edgeOld x = Fin.castAdd 2 x

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inl_adj_old_old {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) (x y : Fin m) : (graftGraph G (Sum.inl e)).Adj (edgeOld x) (edgeOld y) ↔ G.Adj x y ∧ s(x, y) ≠ ↑e

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inl_adj_old_mid {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) (x : Fin m) : (graftGraph G (Sum.inl e)).Adj (edgeOld x) (edgeMidpoint m) ↔ x ∈ ↑e

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inl_adj_mid_new {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) : (graftGraph G (Sum.inl e)).Adj (edgeMidpoint m) (edgeNewLeaf m)

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inl_adj_old_new {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) (x : Fin m) : ¬(graftGraph G (Sum.inl e)).Adj (edgeOld x) (edgeNewLeaf m)

theorem BGW.StableTrees.Marchal.graftGraph_inl_adj_mid_mid {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) : ¬(graftGraph G (Sum.inl e)).Adj (edgeMidpoint m) (edgeMidpoint m)

theorem BGW.StableTrees.Marchal.graftGraph_inl_adj_new_new {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) : ¬(graftGraph G (Sum.inl e)).Adj (edgeNewLeaf m) (edgeNewLeaf m)

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inl_adj_mid_old {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) (x : Fin m) : (graftGraph G (Sum.inl e)).Adj (edgeMidpoint m) (edgeOld x) ↔ x ∈ ↑e

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inl_adj_new_old {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) (x : Fin m) : ¬(graftGraph G (Sum.inl e)).Adj (edgeNewLeaf m) (edgeOld x)

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inl_adj_new_mid {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) : (graftGraph G (Sum.inl e)).Adj (edgeNewLeaf m) (edgeMidpoint m)

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inl_degree_new {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) : (graftGraph G (Sum.inl e)).degree (edgeNewLeaf m) = 1

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inl_degree_mid {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) : (graftGraph G (Sum.inl e)).degree (edgeMidpoint m) = 3

@[simp]

theorem BGW.StableTrees.Marchal.graftGraph_inl_degree_old {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) (x : Fin m) : (graftGraph G (Sum.inl e)).degree (edgeOld x) = G.degree x

theorem BGW.StableTrees.Marchal.graftGraph_inl_isTree {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) (hG : G.IsTree) : (graftGraph G (Sum.inl e)).IsTree

An edge graft subdivides one edge and adds a leaf, hence remains a tree.

theorem BGW.StableTrees.Marchal.graftGraph_inr_isTree {m : ℕ} (G : SimpleGraph (Fin m)) (v : { v : Fin m // 3 ≤ G.degree v }) (hG : G.IsTree) : (graftGraph G (Sum.inr v)).IsTree

A vertex graft adds exactly one edge and preserves connectivity.

def BGW.StableTrees.Marchal.extendLast {n M : ℕ} (f : Fin (n + 1) ↪ Fin M) (z : Fin M) (hz : z ∉ Set.range ⇑f) : Fin (n + 2) ↪ Fin M

Extend a label embedding by a new final label outside its range.

Equations

• BGW.StableTrees.Marchal.extendLast f z hz = { toFun := fun (i : Fin (n + 1 + 1)) => Fin.lastCases z (⇑f) i, inj' := ⋯ }

@[simp]

theorem BGW.StableTrees.Marchal.extendLast_apply_last {n M : ℕ} (f : Fin (n + 1) ↪ Fin M) (z : Fin M) (hz : z ∉ Set.range ⇑f) : (extendLast f z hz) (Fin.last (n + 1)) = z

@[simp]

theorem BGW.StableTrees.Marchal.extendLast_apply_old {n M : ℕ} (f : Fin (n + 1) ↪ Fin M) (z : Fin M) (hz : z ∉ Set.range ⇑f) (i : Fin (n + 1)) : (extendLast f z hz) i.castSucc = f i

theorem BGW.StableTrees.Marchal.range_extendLast {n M : ℕ} (f : Fin (n + 1) ↪ Fin M) (z : Fin M) (hz : z ∉ Set.range ⇑f) (y : Fin M) : y ∈ Set.range ⇑(extendLast f z hz) ↔ y = z ∨ y ∈ Set.range ⇑f

The range after extending labels is the new label together with the old range.

noncomputable def BGW.StableTrees.Marchal.graft {n : ℕ} (T : LTree n) (p : Position T.G) : LTree (n + 1)

The tree obtained by grafting A_{n+1} at a position of T.

Equations

• One or more equations did not get rendered due to their size.