Exact-size walk and height prefix laws

Both coordinates come from one tree, with the sealed terminal walk convention. The restriction and marginal identities identify the law with the existing walk-prefix API.

noncomputable def BGW.StableTrees.ExactPair.exactPairLaw (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (_hn : Admissible μ n) (a : NNReal) : MeasureTheory.ProbabilityMeasure (Skorokhod.D ↑a ℝ × C(↑(Set.Icc 0 ↑a), ℝ))

The exact-size pair law on [0,a]: the (walk, height) pair of ONE BGW tree conditioned on size exactly n (sealed K02 exactTreeLaw, totalized), at scales nt, 1/B n, B n / n.

Equations

• BGW.StableTrees.ExactPair.exactPairLaw μ B n _hn a = (BGW.StableTrees.DiscreteForest.exactTreeLaw μ n).map (BGW.StableTrees.TailPair.treePairPath B n a)

theorem BGW.StableTrees.ExactPair.exactPairLaw_map_fst {μ : PMF ℕ} {B : ℕ → ℝ} {n : ℕ} (hn : Admissible μ n) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : (exactPairLaw μ B n hn a).map Prod.fst = ExactPrefix.exactWalkPrefixLaw μ B n hn a ⋯

The walk marginal of the exact pair law is the sealed K07 exact walk prefix law.

theorem BGW.StableTrees.ExactPair.map_fst_restrictPair_excLaw (θ : ℝ) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : ((excLaw θ).map (restrictPair ⋯)).map Prod.fst = (unitExcursionLaw θ).map (excursionRestrict a)

The walk marginal of the target is the sealed K07 target (every θ).

Prefix-measurability repair

theorem BGW.StableTrees.ExactPair.restrictPair_treePairPath (B : ℕ → ℝ) (n : ℕ) {a a' : NNReal} (h : a ≤ a') (τ : LocallyFinite.Tree) : restrictPair h (TailPair.treePairPath B n a' τ) = TailPair.treePairPath B n a τ

Projectivity (deterministic): the pair path of horizon a' restricted to [0,a] is the pair path of horizon a.