OAI/Topology/ArtinGroups/ParabolicIntersections/TreeSegmentCount.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform counts of free segment translates along shortcut paths.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.segmentOccurrences_branches line 15
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.TreeAction.branch_support_common line 38
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.segmentOccurrences_bound line 52

    Source documentation

    A shortcut walk of length n crosses at most n (2L+1)^2 translates of a free length-L segment, independently of vertex valences.

    theorem segmentOccurrences_bound (hT : T.IsTree) (hA : PreservesAdj (G := G) T)
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.TreeAction.PreservesAdj

  4. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.segmentOccurrences_bound_dist line 115