Local factors in the exact Marchal law

Writing the numerator as a product over all vertices makes its change under each of the two graft operations explicit.

noncomputable def BGW.StableTrees.Marchal.degreeLawFactor (α : ℝ) (d : ℕ) : ℝ

Contribution of a degree to the numerator, with contribution one for leaves.

Equations

• BGW.StableTrees.Marchal.degreeLawFactor α d = if 3 ≤ d then (α - 1) * ∏ j ∈ Finset.Icc 2 (d - 2), (↑j - α) else 1

@[simp]

theorem BGW.StableTrees.Marchal.degreeLawFactor_one (α : ℝ) : degreeLawFactor α 1 = 1

@[simp]

theorem BGW.StableTrees.Marchal.degreeLawFactor_three (α : ℝ) : degreeLawFactor α 3 = α - 1

theorem BGW.StableTrees.Marchal.degreeLawFactor_succ (α : ℝ) {d : ℕ} (hd : 3 ≤ d) : degreeLawFactor α (d + 1) = degreeLawFactor α d * (↑d - 1 - α)

Increasing an internal degree contributes the next Marchal vertex weight.

theorem BGW.StableTrees.Marchal.LTree.lawWeight_eq_prod {n : ℕ} (T : LTree n) (α : ℝ) : lawWeight α T = ∏ v : Fin T.m, degreeLawFactor α (T.G.degree v)

The law numerator is a product of local degree factors over all vertices.

theorem BGW.StableTrees.Marchal.LTree.lawWeight_graft_inl {n : ℕ} (T : LTree n) (α : ℝ) (e : ↑T.G.edgeSet) : lawWeight α (graft T (Sum.inl e)) = lawWeight α T * (α - 1)

Grafting on an edge multiplies the exact-law numerator by its selection weight.

theorem BGW.StableTrees.Marchal.LTree.lawWeight_graft_inr {n : ℕ} (T : LTree n) (α : ℝ) (v : { v : Fin T.m // 3 ≤ T.G.degree v }) : lawWeight α (graft T (Sum.inr v)) = lawWeight α T * (↑(T.G.degree ↑v) - 1 - α)

Grafting on an internal vertex multiplies the numerator by its selection weight.

theorem BGW.StableTrees.Marchal.LTree.lawWeight_graft {n : ℕ} (T : LTree n) (α : ℝ) (p : Position T.G) : lawWeight α (graft T p) = lawWeight α T * selectionWeight T.G α p

Every graft contributes exactly the selected Marchal weight to the numerator.