Documentation

BGW.ContinuumTrees.UniformVertexSampling

Uniform sampling of vertices by DFS rank #

A time in the unit interval selects DFS rank min (floor (size * time)) (size - 1). The final time therefore selects the last vertex. All earlier rank cells are half-open intervals of length 1 / size; the final cell is closed at one and has the same volume. The pushforward of the actual interval volume is exactly the uniform measure on all vertices, including roots and leaves.

source
noncomputable def BGW.ContinuumTrees.FiniteTree.sampleVertex (t : PlaneTree) (s : ↑unitInterval) :
t.Vertex

Select a DFS vertex by an interval time, with the final time clamped to the last rank.

Equations
Instances For
    source
    theorem BGW.ContinuumTrees.FiniteTree.measurable_sampleVertex (t : PlaneTree) :
    Measurable (sampleVertex t)

    The sampler is measurable into the existing Borel space of vertices.

    source
    theorem BGW.ContinuumTrees.FiniteTree.map_sampleVertex_volume (t : PlaneTree) :
    MeasureTheory.Measure.map (sampleVertex t) MeasureTheory.volume = ↑(mass t)

    Interval volume pushes forward to exactly the uniform probability on all vertices.

    source
    @[simp]
    theorem BGW.ContinuumTrees.FiniteTree.sampleVertex_zero (t : PlaneTree) :
    sampleVertex t 0 = root t

    The first sampling time selects the root.

    source
    theorem BGW.ContinuumTrees.FiniteTree.sampleVertex_surjective (t : PlaneTree) :
    Function.Surjective (sampleVertex t)

    Every vertex is selected, at the time given by its DFS rank divided by tree size.

    source
    theorem BGW.ContinuumTrees.FiniteTree.abs_vertexTime_sampleVertex_sub_le (t : PlaneTree) (hn : 2 ≤ t.size) (s : ↑unitInterval) :
    |↑(vertexTime t (sampleVertex t s)) - ↑s| ≤ ‖t.contourFunction‖ / (2 * ↑(t.size - 1)) + 2 / ↑t.size

    The sampled vertex's first-visit time stays uniformly close to its sampling time.