Marchal law along its unique histories

The unique-parent and injective-position lemmas reduce the mass of a graft to a single term in the transition and in the bind defining the chain.

Every labelled state has a graft decomposition. Induction therefore gives the all-state product formula, and the binary specialization gives the exact count of binary states by normalization of the probability mass function.

Each state has a unique history (remove the last leaf and suppress the resulting degree-two vertex), so its probability is a single product of selection weights. References: P. Marchal, A note on the fragmentation of a stable tree, DMTCS Proc. (2008); N. Curien and B. Haas, The stable trees are nested, arXiv:1207.5418, §§1.1, 1.3.

theorem BGW.StableTrees.Marchal.step_apply_graft {k : ℕ} {α : ℝ} (hα : 1 < α) (hα2 : α ≤ 2) (T : LTree (k + 1)) (p : Position T.G) : (step hα hα2 k ⟦T⟧) ⟦graft T p⟧ = ENNReal.ofReal (selectionWeight T.G α p) / ENNReal.ofReal (↑(k + 1) * α - 1)

A graft has exactly the mass of the position that produced it.

theorem BGW.StableTrees.Marchal.step_apply_graft_of_ne {k : ℕ} {α : ℝ} (hα : 1 < α) (hα2 : α ≤ 2) (T : LTree (k + 1)) (p : Position T.G) (s : State (k + 1)) (hs : s ≠ ⟦T⟧) : (step hα hα2 k s) ⟦graft T p⟧ = 0

A transition to a given graft vanishes at every other parent state.

theorem BGW.StableTrees.Marchal.law_apply_graft {k : ℕ} {α : ℝ} (hα : 1 < α) (hα2 : α ≤ 2) (T : LTree (k + 1)) (p : Position T.G) : (law hα hα2 (k + 1)) ⟦graft T p⟧ = (law hα hα2 k) ⟦T⟧ * (ENNReal.ofReal (selectionWeight T.G α p) / ENNReal.ofReal (↑(k + 1) * α - 1))

The probability recurrence has a single parent and a single position.

theorem BGW.StableTrees.Marchal.startState_lawWeight (α : ℝ) : State.lawWeight α startState = 1

The numerator on the initial edge is one.

theorem BGW.StableTrees.Marchal.law_denominator_pos {α : ℝ} (hα : 1 < α) (k : ℕ) : 0 < ∏ j ∈ Finset.range k, (↑(j + 1) * α - 1)

The normalizing product is strictly positive throughout the stable range.

theorem BGW.StableTrees.Marchal.law_apply_graft_of_formula {k : ℕ} {α : ℝ} (hα : 1 < α) (hα2 : α ≤ 2) (T : LTree (k + 1)) (p : Position T.G) (hT : (law hα hα2 k) ⟦T⟧ = ENNReal.ofReal (LTree.lawWeight α T / ∏ j ∈ Finset.range k, (↑(j + 1) * α - 1))) : (law hα hα2 (k + 1)) ⟦graft T p⟧ = ENNReal.ofReal (LTree.lawWeight α (graft T p) / ∏ j ∈ Finset.range (k + 1), (↑(j + 1) * α - 1))

The product formula propagates from a parent to any one of its grafts.

theorem BGW.StableTrees.Marchal.law_apply_of_mem_support {α : ℝ} (hα : 1 < α) (hα2 : α ≤ 2) (k : ℕ) (s : State (k + 1)) (hs : s ∈ (law hα hα2 k).support) : (law hα hα2 k) s = ENNReal.ofReal (State.lawWeight α s / ∏ j ∈ Finset.range k, (↑(j + 1) * α - 1))

The exact product formula holds at every state in the support of the chain.

theorem BGW.StableTrees.Marchal.law_two_apply_of_mem_support (k : ℕ) (s : State (k + 1)) (hs : s ∈ (law law_two_apply_of_mem_support._proof_1 ⋯ k).support) : (law law_two_apply_of_mem_support._proof_1 ⋯ k) s = (↑(2 * (k + 1) - 3).doubleFactorial)⁻¹

At index two every supported state has the double-factorial mass.

theorem BGW.StableTrees.Marchal.ncard_law_two_support (k : ℕ) : (law law_two_apply_of_mem_support._proof_1 ⋯ k).support.ncard = (2 * (k + 1) - 3).doubleFactorial

The number of supported states at index two is the double factorial.

theorem BGW.StableTrees.Marchal.law_apply {α : ℝ} (hα : 1 < α) (hα2 : α ≤ 2) (k : ℕ) (s : State (k + 1)) : (law hα hα2 k) s = ENNReal.ofReal (State.lawWeight α s / ∏ j ∈ Finset.range k, (↑(j + 1) * α - 1))

Exact finite-tree law of the Marchal chain. Step n = k+1; denominator the denominator ∏_{j=1}^{k} (j α - 1) is written as ∏_{j<k} ((j+1) α - 1).

theorem BGW.StableTrees.Marchal.law_two_binary_apply (k : ℕ) (s : State (k + 1)) (hs : s.IsBinary) : (law law_two_apply_of_mem_support._proof_1 ⋯ k) s = (↑(2 * (k + 1) - 3).doubleFactorial)⁻¹

α = 2: Rémy's law — uniform on binary states, mass 1/(2n-3)!! with n = k+1.

theorem BGW.StableTrees.Marchal.ncard_binary_states (k : ℕ) : {s : State (k + 1) | s.IsBinary}.ncard = (2 * (k + 1) - 3).doubleFactorial

There are (2n-3)!! binary leaf-labelled trees with leaves A_0..A_n, n = k+1 (with (-1)!! = 1 read as 0‼ = 1; checked at n = 1,2,3: 1, 1, 3).