Documentation

BGW.ContinuumTrees.ContourEmbedding

Isometric embedding of vertices in their contour-coded tree #

A vertex is represented by its first contour visit. The minimum between two such visits is their common ancestor's depth, so the coding distance agrees with the graph metric. The embedding preserves the root. Its mass comparison with the contour's Lebesgue pushforward is a separate result.

source
noncomputable def BGW.ContinuumTrees.FiniteTree.vertexTime (t : PlaneTree) (u : t.Vertex) :
↑unitInterval

Time of the first visit to a present vertex, in the normalized contour traversal.

Equations
Instances For
    source
    theorem BGW.ContinuumTrees.FiniteTree.contourFunction_vertexTime (t : PlaneTree) (u : t.Vertex) :
    t.contourFunction (vertexTime t u) = ↑(↑u).length

    The continuous contour at a vertex's first visit records its depth.

    source
    noncomputable def BGW.ContinuumTrees.FiniteTree.vertexEmbedding (t : PlaneTree) (u : t.Vertex) :
    Coding.Space t.contourFunction

    The image of a vertex in the real tree coded by the interpolated contour.

    Equations
    Instances For
      source
      theorem BGW.ContinuumTrees.FiniteTree.isometry_vertexEmbedding (t : PlaneTree) :
      Isometry (vertexEmbedding t)

      The contour-coded distance between vertices is exactly their existing graph metric.

      source
      @[simp]
      theorem BGW.ContinuumTrees.FiniteTree.vertexTime_root (t : PlaneTree) :
      vertexTime t (root t) = 0
      source
      @[simp]
      theorem BGW.ContinuumTrees.FiniteTree.vertexEmbedding_root (t : PlaneTree) :
      vertexEmbedding t (root t) = Coding.root t.contourFunction

      The embedding sends the finite tree's root to the coding root.

      source
      theorem BGW.ContinuumTrees.FiniteTree.duration_mul_vertexTime_add_depth (t : PlaneTree) (u : t.Vertex) :
      ↑(t.contour.length - 1) * ↑(vertexTime t u) + ↑(↑u).length = 2 * ↑(List.idxOf (↑u) t.vertices)

      The addition-only relation between first-visit time, depth and DFS index.

      source
      theorem BGW.ContinuumTrees.FiniteTree.abs_vertexTime_sub_dfsTime_le (t : PlaneTree) (hn : 2 ≤ t.size) (u : t.Vertex) :
      |↑(vertexTime t u) - ↑(List.idxOf (↑u) t.vertices) / ↑t.size| ≤ ↑(↑u).length / (2 * ↑(t.size - 1)) + 1 / ↑t.size

      First-visit time is close to normalized DFS rank when depth is small relative to size.