Reindexing Marchal trees

Equivalences of finite vertex sets transport both graphs and leaf labels. Swaps then place the leaf to be pruned, and optionally its neighbour, last.

noncomputable def BGW.StableTrees.Marchal.LTree.reindex {n m : ℕ} (T : LTree n) (e : Fin m ≃ Fin T.m) : LTree n

Transport a labelled tree along an equivalence from the new vertex set.

Equations

• T.reindex e = { m := m, G := SimpleGraph.comap (⇑e) T.G, tree := ⋯, labels := T.labels.trans e.symm.toEmbedding, leaf := ⋯, branch := ⋯ }

theorem BGW.StableTrees.Marchal.LTree.reindex_state {n m : ℕ} (T : LTree n) (e : Fin m ≃ Fin T.m) : ⟦T.reindex e⟧ = ⟦T⟧

Reindexing preserves the labelled state.

theorem BGW.StableTrees.Marchal.state_one_eq_start (s : State 1) : s = startState

Every state with two labelled leaves is the initial edge.

noncomputable def BGW.StableTrees.Marchal.placeLast {m M : ℕ} (e : Fin (m + 1) ≃ Fin M) (z : Fin M) : Fin (m + 1) ≃ Fin M

A swap places a specified vertex last under a given indexing equivalence.

Equations

• BGW.StableTrees.Marchal.placeLast e z = e.trans (Equiv.swap (e (Fin.last m)) z)

@[simp]

theorem BGW.StableTrees.Marchal.placeLast_last {m M : ℕ} (e : Fin (m + 1) ≃ Fin M) (z : Fin M) : (placeLast e z) (Fin.last m) = z

noncomputable def BGW.StableTrees.Marchal.placeLastTwo {m M : ℕ} (e : Fin (m + 2) ≃ Fin M) (z u : Fin M) : Fin (m + 2) ≃ Fin M

Two swaps place distinct specified vertices at the midpoint and last indices.

Equations

• BGW.StableTrees.Marchal.placeLastTwo e z u = Equiv.trans (Equiv.swap (Fin.last m).castSucc ((BGW.StableTrees.Marchal.placeLast e z).symm u)) (BGW.StableTrees.Marchal.placeLast e z)

@[simp]

theorem BGW.StableTrees.Marchal.placeLastTwo_mid {m M : ℕ} (e : Fin (m + 2) ≃ Fin M) (z u : Fin M) : (placeLastTwo e z u) (Fin.last m).castSucc = u

@[simp]

theorem BGW.StableTrees.Marchal.placeLastTwo_last {m M : ℕ} (e : Fin (m + 2) ≃ Fin M) (z u : Fin M) (hzu : z ≠ u) : (placeLastTwo e z u) (Fin.last (m + 1)) = z