Marchal selection weights on a finite labelled tree

The graph is an existing finite SimpleGraph, with its leaves enumerated injectively by Fin (n + 1). Positions are edges or vertices of degree at least three. No plane order, tree-state quotient, or growth operation is introduced here.

The intended selection weights are those of Curien–Haas, The stable trees are nested, arXiv:1207.5418v1, Section 1.3, equation (2): an edge has weight α - 1, and a vertex of degree d ≥ 3 has weight d - 1 - α.

@[reducible, inline]

abbrev BGW.StableTrees.Marchal.Position {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : Type u_1

The existing graph's edges and internal vertices, as distinct selection positions.

Equations

• BGW.StableTrees.Marchal.Position G = (↑G.edgeSet ⊕ { v : V // 3 ≤ G.degree v })

def BGW.StableTrees.Marchal.selectionWeight {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (α : ℝ) : Position G → ℝ

Marchal's real selection weight at one edge or one internal vertex.

Equations

• BGW.StableTrees.Marchal.selectionWeight G α (Sum.inl val) = α - 1
• BGW.StableTrees.Marchal.selectionWeight G α (Sum.inr v) = ↑(G.degree ↑v) - 1 - α

theorem BGW.StableTrees.Marchal.selectionWeight_nonneg {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {α : ℝ} (hα : 1 < α) (hα2 : α ≤ 2) (p : Position G) : 0 ≤ selectionWeight G α p

Every selectable position has nonnegative weight throughout the stable parameter range.

theorem BGW.StableTrees.Marchal.sum_selectionWeight {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {n : ℕ} (hT : G.IsTree) (labels : Fin (n + 1) ↪ V) (hleaf : ∀ (v : V), G.degree v = 1 ↔ v ∈ Set.range ⇑labels) (hbranch : ∀ (v : V), G.degree v ≠ 1 → 3 ≤ G.degree v) (α : ℝ) : ∑ p : Position G, selectionWeight G α p = ↑n * α - 1

Exhaustive leaf labels and the absence of other small degrees give the exact total weight. This identity is algebraic in α; its positivity is a separate result.

theorem BGW.StableTrees.Marchal.normalizer_pos {n : ℕ} (hn : 1 ≤ n) {α : ℝ} (hα : 1 < α) : 0 < ↑n * α - 1

The Marchal normalizer is strictly positive at every valid starting index.

noncomputable def BGW.StableTrees.Marchal.selectionPMF {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {n : ℕ} (hT : G.IsTree) (labels : Fin (n + 1) ↪ V) (hleaf : ∀ (v : V), G.degree v = 1 ↔ v ∈ Set.range ⇑labels) (hbranch : ∀ (v : V), G.degree v ≠ 1 → 3 ≤ G.degree v) (hn : 1 ≤ n) (α : ℝ) (hα : 1 < α) (hα2 : α ≤ 2) : PMF (Position G)

The normalized Marchal selection law on the graph's actual edges and internal vertices.

Equations

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

@[simp]

theorem BGW.StableTrees.Marchal.selectionPMF_apply {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {n : ℕ} (hT : G.IsTree) (labels : Fin (n + 1) ↪ V) (hleaf : ∀ (v : V), G.degree v = 1 ↔ v ∈ Set.range ⇑labels) (hbranch : ∀ (v : V), G.degree v ≠ 1 → 3 ≤ G.degree v) (hn : 1 ≤ n) (α : ℝ) (hα : 1 < α) (hα2 : α ≤ 2) (p : Position G) : (selectionPMF G hT labels hleaf hbranch hn α hα hα2) p = ENNReal.ofReal (selectionWeight G α p) / ENNReal.ofReal (↑n * α - 1)

Each atom is its nonnegative real selection weight divided by n * α - 1.