OAI/Topology/ArtinGroups/ParabolicIntersections/TreeBallCount.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniformly bounded intersections of a tree path with a metric ball.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.path_prefix_dist line 12
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.path_index_dist line 19
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.path_ball_ncard line 31

    Source documentation

    Even in a tree of infinite valence, a radius-L ball meets a simple path in at most 2L+1 vertices.

    theorem path_ball_ncard (hT : T.IsTree) {x y b : V}
    (p : T.Walk x y) (hp : p.IsPath) (hb : b∈p.support) (L : ℕ) :
    {w | w∈p.support ∧ T.dist b w≤L}.ncard≤2*L+1 := by
…