Functoriality of the Marchal step

A labelled graph isomorphism transports selection positions and induces an isomorphism after grafting. The representative transition therefore descends to the quotient state space.

def BGW.StableTrees.Marchal.edgeVertexCongr {m m' : ℕ} (e : Fin m ≃ Fin m') : Fin (m + 2) ≃ Fin (m' + 2)

Transport of old, midpoint and new vertices under an equivalence.

Equations

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

def BGW.StableTrees.Marchal.vertexVertexCongr {m m' : ℕ} (e : Fin m ≃ Fin m') : Fin (m + 1) ≃ Fin (m' + 1)

Transport of old and new vertices under an equivalence.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem BGW.StableTrees.Marchal.inl_adj_new_mid_cast {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) : (graftGraph G (Sum.inl e)).Adj (Fin.last (m + 1)) (Fin.last m).castSucc

@[simp]

theorem BGW.StableTrees.Marchal.inl_adj_new_old_cast {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) (x : Fin m) : ¬(graftGraph G (Sum.inl e)).Adj (Fin.last (m + 1)) x.castSucc.castSucc

@[simp]

theorem BGW.StableTrees.Marchal.inl_adj_mid_new_cast {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) : (graftGraph G (Sum.inl e)).Adj (Fin.last m).castSucc (Fin.last (m + 1))

@[simp]

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

@[simp]

theorem BGW.StableTrees.Marchal.inl_adj_old_new_cast {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) (x : Fin m) : ¬(graftGraph G (Sum.inl e)).Adj x.castSucc.castSucc (Fin.last (m + 1))

@[simp]

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

@[simp]

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

noncomputable def BGW.StableTrees.Marchal.positionCongr {n : ℕ} {T T' : LTree n} (e : T.G ≃g T'.G) : Position T.G ≃ Position T'.G

The positions transported by a graph isomorphism.

Equations

• BGW.StableTrees.Marchal.positionCongr e = e.mapEdgeSet.sumCongr (BGW.StableTrees.Marchal.LTree.internalEquiv e)

noncomputable def BGW.StableTrees.Marchal.graftVertexIso {n : ℕ} {T T' : LTree n} (e : T.G ≃g T'.G) (v : { v : Fin T.m // 3 ≤ T.G.degree v }) : graftGraph T.G (Sum.inr v) ≃g graftGraph T'.G (Sum.inr ((LTree.internalEquiv e) v))

Grafting on corresponding branch vertices gives isomorphic graphs.

Equations

• BGW.StableTrees.Marchal.graftVertexIso e v = { toEquiv := BGW.StableTrees.Marchal.vertexVertexCongr e.toEquiv, map_rel_iff' := ⋯ }

noncomputable def BGW.StableTrees.Marchal.graftEdgeIso {n : ℕ} {T T' : LTree n} (e : T.G ≃g T'.G) (a : ↑T.G.edgeSet) : graftGraph T.G (Sum.inl a) ≃g graftGraph T'.G (Sum.inl (e.mapEdgeSet a))

Grafting on corresponding edges gives isomorphic graphs.

Equations

• BGW.StableTrees.Marchal.graftEdgeIso e a = { toEquiv := BGW.StableTrees.Marchal.edgeVertexCongr e.toEquiv, map_rel_iff' := ⋯ }

@[simp]

theorem BGW.StableTrees.Marchal.graft_labels_last {n : ℕ} (T : LTree n) (p : Position T.G) : (graft T p).labels (Fin.last (n + 1)) = match p with | Sum.inl val => edgeNewLeaf T.m | Sum.inr val => vertexNewLeaf T.m

@[simp]

theorem BGW.StableTrees.Marchal.graft_labels_old {n : ℕ} (T : LTree n) (p : Position T.G) (i : Fin (n + 1)) : (graft T p).labels i.castSucc = match p with | Sum.inl val => edgeOld (T.labels i) | Sum.inr val => vertexOld (T.labels i)

theorem BGW.StableTrees.Marchal.graft_congr {n : ℕ} {T T' : LTree n} (e : T.G ≃g T'.G) (he : ∀ (i : Fin (n + 1)), e (T.labels i) = T'.labels i) (p : Position T.G) : ⟦graft T p⟧ = ⟦graft T' ((positionCongr e) p)⟧

Grafting commutes with labelled isomorphism, through positionCongr.

noncomputable def BGW.StableTrees.Marchal.stepRep {k : ℕ} {α : ℝ} (hα : 1 < α) (hα2 : α ≤ 2) (T : LTree (k + 1)) : PMF (State (k + 2))

One Marchal step on a representative: select a position (selectionPMF), graft, take class.

Equations

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

theorem BGW.StableTrees.Marchal.stepRep_congr {k : ℕ} {α : ℝ} (hα : 1 < α) (hα2 : α ≤ 2) {T T' : LTree (k + 1)} (h : T ≈ T') : stepRep hα hα2 T = stepRep hα hα2 T'

Grafting commutes with labelled isomorphism, up to the induced bijection of positions.

noncomputable def BGW.StableTrees.Marchal.step {α : ℝ} (hα : 1 < α) (hα2 : α ≤ 2) (k : ℕ) : State (k + 1) → PMF (State (k + 2))

The transition kernel State (k+1) → PMF (State (k+2)).

Equations

• BGW.StableTrees.Marchal.step hα hα2 k = Quotient.lift (BGW.StableTrees.Marchal.stepRep hα hα2) ⋯

theorem BGW.StableTrees.Marchal.sum_selectionWeight_step {k : ℕ} (T : LTree (k + 1)) (α : ℝ) : ∑ p : Position T.G, selectionWeight T.G α p = ↑(k + 1) * α - 1

Total selection weight at step n = k+1 is n α - 1.

noncomputable def BGW.StableTrees.Marchal.law {α : ℝ} (hα : 1 < α) (hα2 : α ≤ 2) (k : ℕ) : PMF (State (k + 1))

The law of the state with leaves A_0..A_{k+1}, started from the edge A_0 — A_1.

Equations

• BGW.StableTrees.Marchal.law hα hα2 0 = PMF.pure BGW.StableTrees.Marchal.startState
• BGW.StableTrees.Marchal.law hα hα2 k.succ = (BGW.StableTrees.Marchal.law hα hα2 k).bind (BGW.StableTrees.Marchal.step hα hα2 k)