OAI/Topology/ArtinGroups/ParabolicIntersections/TreeSegmentBallCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform counts for translates of a free segment near a path vertex.

  1. def OAI.HarmonicArtin.ParabolicIntersections.TreeAction.localSegmentOccurrences line 11
  2. theorem OAI.HarmonicArtin.ParabolicIntersections.TreeAction.localSegmentOccurrences_bound line 16

    Source documentation

    The bound is independent of the path length and of vertex valences.

    theorem localSegmentOccurrences_bound (hT : T.IsTree)
    (hfree : pairStabilizer (G := G) u v=⊥)
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.TreeAction.pairStabilizer