The joint prefix density at a larger horizon

A smaller pair prefix is measurable in the larger degree prefix. The discrete prefix Radon–Nikodym identity therefore transfers to the pair after restriction.

theorem BGW.StableTrees.ExactPair.exactPairLaw_eq_map_withDensity {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {n : ℕ} (hn : Admissible μ n) {a a' : NNReal} (haa' : a ≤ a') (ha' : a' ∈ Set.Ioo 0 1) (hm : ⌊↑a * ↑n⌋₊ + 1 ≤ ⌊↑a' * ↑n⌋₊) : ↑(exactPairLaw μ B n hn a) = MeasureTheory.Measure.map (restrictPair haa') ((↑(TailPair.tailPairLaw μ B n a')).withDensity fun (z : Skorokhod.D ↑a' ℝ × C(↑(Set.Icc 0 ↑a'), ℝ)) => ENNReal.ofReal (ExactPrefix.prefixWeightFn μ B n a' z.1))

Weighted identity at a larger horizon (the repair): for a ≤ a' < 1 with ⌊an⌋ + 1 ≤ ⌊a'n⌋, the exact pair law on [0,a] is the [0,a]-restriction of the tail pair law on [0,a'] weighted by the sealed walk weight at a' (a function of the walk value at a').