Reversal of the bridge offspring vector

Reindexing the iid product by the reversing permutation preserves its law and the bridge event. Reversed partial sums describe the terminal window exactly.

def BGW.StableTrees.DiscreteBridge.reverseVec {n : ℕ} (ω : Fin n → ℕ) : Fin n → ℕ

Reverse the order of the offspring counts.

Equations

• BGW.StableTrees.DiscreteBridge.reverseVec ω i = ω i.rev

theorem BGW.StableTrees.DiscreteBridge.measurable_reverseVec (n : ℕ) : Measurable reverseVec

Reversal is a measurable involution on offspring vectors.

theorem BGW.StableTrees.DiscreteBridge.stepWord_reverseVec {n : ℕ} (ω : Fin n → ℕ) : stepWord (reverseVec ω) = (stepWord ω).reverse

The Łukasiewicz word of the reversed vector is the reversed word.

theorem BGW.StableTrees.DiscreteBridge.reverseVec_mem_countBridges_iff {n : ℕ} (ω : Fin n → ℕ) : reverseVec ω ∈ countBridges n ↔ ω ∈ countBridges n

Reversing a vector preserves the bridge event.

theorem BGW.StableTrees.DiscreteBridge.map_reverseVec_offspringVec (μ : PMF ℕ) (n : ℕ) : MeasureTheory.Measure.map reverseVec (offspringVec μ n) = offspringVec μ n

Reversal preserves the iid offspring-vector law.

theorem BGW.StableTrees.DiscreteBridge.map_reverseVec_cond_countBridges (μ : PMF ℕ) (n : ℕ) : MeasureTheory.Measure.map reverseVec (offspringVec μ n)[|countBridges n] = (offspringVec μ n)[|countBridges n]

The bridge-conditioned offspring vector has the same law when reversed.

theorem BGW.StableTrees.DiscreteBridge.sum_take_stepWord_reverseVec {n k : ℕ} (ω : Fin n → ℕ) (hk : k ≤ n) : (List.take (n - k) (stepWord (reverseVec ω))).sum = (stepWord ω).sum - (List.take k (stepWord ω)).sum

Reversed prefix sums are the full sum minus the corresponding original prefix.