Documentation

BGW.ContinuumTrees.FiniteTree

Finite plane trees as rooted compact metric probability spaces #

The carrier is the existing subtype PlaneTree.Vertex t of present addresses, with its graph metric. Its Borel probability measure gives mass 1 / t.size to every vertex, including the root and all leaves. No measurable structure on the type of plane trees or on all addresses is introduced.

This module only bundles the finite tree. Metric scaling and comparison with a continuously coded tree are separate constructions.

source
@[instance_reducible]
noncomputable instance BGW.ContinuumTrees.FiniteTree.vertexFintype (t : PlaneTree) :
Fintype t.Vertex

Enumerate the existing vertex subtype using the DFS address list.

Equations
source
@[simp]
theorem BGW.ContinuumTrees.FiniteTree.card_vertex (t : PlaneTree) :
Fintype.card t.Vertex = t.size

Cardinality counts all vertex occurrences, including the root.

source
def BGW.ContinuumTrees.FiniteTree.root (t : PlaneTree) :
t.Vertex

The distinguished root address.

Equations
Instances For
    source
    instance BGW.ContinuumTrees.FiniteTree.vertexNonempty (t : PlaneTree) :
    Nonempty t.Vertex
    source
    @[instance_reducible]
    noncomputable instance BGW.ContinuumTrees.FiniteTree.vertexMeasurableSpace (t : PlaneTree) :
    MeasurableSpace t.Vertex

    Use the Borel structure of the existing graph metric.

    Equations
    source
    instance BGW.ContinuumTrees.FiniteTree.vertexBorelSpace (t : PlaneTree) :
    BorelSpace t.Vertex
    source
    noncomputable def BGW.ContinuumTrees.FiniteTree.mass (t : PlaneTree) :
    MeasureTheory.ProbabilityMeasure t.Vertex

    Uniform probability on every vertex of the finite tree.

    Equations
    Instances For
      source
      @[simp]
      theorem BGW.ContinuumTrees.FiniteTree.coe_mass (t : PlaneTree) :
      ↑(mass t) = MeasureTheory.Measure.uniformOfFinset Finset.univ
      source
      theorem BGW.ContinuumTrees.FiniteTree.mass_singleton (t : PlaneTree) (u : t.Vertex) :
      ↑(mass t) {u} = (↑t.size)⁻¹

      Each present vertex has the same positive mass, regardless of its degree.

      source
      noncomputable def BGW.ContinuumTrees.FiniteTree.compactMeasuredSpace (t : PlaneTree) :
      MetricMeasure.CompactMeasuredSpace

      The whole finite vertex space with its graph metric and uniform probability.

      Equations
      Instances For
        source
        noncomputable def BGW.ContinuumTrees.FiniteTree.rootedCompactMeasuredSpace (t : PlaneTree) :
        MetricMeasure.RootedCompactMeasuredSpace

        The same measured vertex space, rooted at the empty address.

        Equations
        Instances For