Basic finite labelled trees for the Marchal chain

This module defines labelled trees, their quotient by label-preserving graph isomorphism, the initial edge, and the weight invariant used in Marchal's exact law.

structure BGW.StableTrees.Marchal.LTree (n : ℕ) : Type

Finite leaf-labelled trees with leaves exactly A_0, …, A_n and no degree-two vertex.

• m : ℕ

  Number of vertices.

• G : SimpleGraph (Fin self.m)

  The tree.

• tree : self.G.IsTree
• labels : Fin (n + 1) ↪ Fin self.m

  Leaf A_i is the vertex labels i.

• leaf (v : Fin self.m) : self.G.degree v = 1 ↔ v ∈ Set.range ⇑self.labels
• branch (v : Fin self.m) : self.G.degree v ≠ 1 → 3 ≤ self.G.degree v

@[instance_reducible]

instance BGW.StableTrees.Marchal.LTree.setoid (n : ℕ) : Setoid (LTree n)

Label-preserving graph isomorphism.

Equations

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

@[reducible, inline]

abbrev BGW.StableTrees.Marchal.State (n : ℕ) : Type

Marchal states at step n: trees with leaves A_0..A_n, modulo labelled isomorphism.

Equations

• BGW.StableTrees.Marchal.State n = Quotient (BGW.StableTrees.Marchal.LTree.setoid n)

def BGW.StableTrees.Marchal.startState : State 1

The start state: the single edge A_0 — A_1.

Equations

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

noncomputable def BGW.StableTrees.Marchal.LTree.internalCount {n : ℕ} (T : LTree n) : ℕ

Number of vertices of degree ≥ 3.

Equations

• T.internalCount = Fintype.card { v : Fin T.m // 3 ≤ T.G.degree v }

noncomputable def BGW.StableTrees.Marchal.LTree.lawWeight {n : ℕ} (α : ℝ) (T : LTree n) : ℝ

Numerator of the exact law: (α-1)^{#internal} ∏_v ∏_{j=2}^{deg v - 2} (j - α).

Equations

• BGW.StableTrees.Marchal.LTree.lawWeight α T = (α - 1) ^ T.internalCount * ∏ v : { v : Fin T.m // 3 ≤ T.G.degree v }, ∏ j ∈ Finset.Icc 2 (T.G.degree ↑v - 2), (↑j - α)

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

The equivalence on internal vertices induced by a graph isomorphism.

Equations

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

theorem BGW.StableTrees.Marchal.LTree.lawWeight_congr {n : ℕ} (α : ℝ) {T T' : LTree n} (h : T ≈ T') : lawWeight α T = lawWeight α T'

The weight is invariant under labelled isomorphism.

noncomputable def BGW.StableTrees.Marchal.State.lawWeight {n : ℕ} (α : ℝ) : State n → ℝ

Numerator of the exact law on states.

Equations

• BGW.StableTrees.Marchal.State.lawWeight α = Quotient.lift (BGW.StableTrees.Marchal.LTree.lawWeight α) ⋯

def BGW.StableTrees.Marchal.State.IsBinary {n : ℕ} : State n → Prop

A state is binary if every vertex has degree one or three.

Equations

• BGW.StableTrees.Marchal.State.IsBinary = Quotient.lift (fun (T : BGW.StableTrees.Marchal.LTree n) => ∀ (v : Fin T.m), T.G.degree v = 1 ∨ T.G.degree v = 3) ⋯