Exact-size tree prefixes and their path encoding

The finite tree correspondence identifies the vector path with the tree prefix on the same sample-size time scale.

instance BGW.StableTrees.ExactPrefix.instIsProbabilityMeasureForallFinNatOffspringVec (μ : PMF ℕ) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (DiscreteBridge.offspringVec μ n)

The shared offspring-vector measure is a probability measure.

theorem BGW.StableTrees.ExactPrefix.sum_range_getD (l : List ℤ) (k : ℕ) : ∑ i ∈ Finset.range k, ↑(l.getD i 0) = ↑(List.take k l).sum

Partial sums of a padded integer list.

theorem BGW.StableTrees.ExactPrefix.treeIncrements_toLocallyFinite (t : PlaneTree) : PathTail.treeIncrements t.toLocallyFinite = t.increments

The tree increments of a finite tree are its plane-tree increments.

@[reducible, inline]

noncomputable abbrev BGW.StableTrees.ExactPrefix.exactWalkPrefixLaw (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (hn : Admissible μ n) (a : NNReal) (ha : a ≤ 1) : MeasureTheory.ProbabilityMeasure (Skorokhod.D ↑a ℝ)

The law of the exact-size walk path on [0,a].

Equations

• BGW.StableTrees.ExactPrefix.exactWalkPrefixLaw μ B n hn a ha = BGW.StableTrees.DiscreteBridge.restrictLaw a ha (BGW.StableTrees.DiscreteBridge.exactWalkLaw μ B n hn)

theorem BGW.StableTrees.ExactPrefix.exactWalkPrefixLaw_eq_map_exactTreeLaw {μ : PMF ℕ} {B : ℕ → ℝ} {n : ℕ} (hn : Admissible μ n) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : ↑(exactWalkPrefixLaw μ B n hn a ⋯) = MeasureTheory.Measure.map (PathTail.treePrefixPath B n a) ↑(DiscreteForest.exactTreeLaw μ n)

The exact-size walk prefix is the prefix path of the exact-size BGW tree: one object.