OAI/Topology/ArtinGroups/ParabolicIntersections/DynamicsDefinitions.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Acylindrical actions and visual splittings

The definitions below spell out the metric content of acylindrical hyperbolicity. Non-elementarity means that an orbit has three distinct Gromov-boundary limit points, represented by Gromov sequences whose pairwise mixed products are bounded. No dynamical assertion is built into a definition of an Artin group.

  1. def OAI.HarmonicArtin.ParabolicIntersections.gromovProduct line 17

    Also declared: ComparatorChallenges/ArtinParabolicIntersections.lean:49 (same declaration text).

  2. def OAI.HarmonicArtin.ParabolicIntersections.IsGromovHyperbolic line 20

    Also declared: ComparatorChallenges/ArtinParabolicIntersections.lean:52 (same declaration text).

  3. def OAI.HarmonicArtin.ParabolicIntersections.IsGeodesicMetric line 24

    Also declared: ComparatorChallenges/ArtinParabolicIntersections.lean:56 (same declaration text).

  4. def OAI.HarmonicArtin.ParabolicIntersections.IsGromovSequence line 28

    Also declared: ComparatorChallenges/ArtinParabolicIntersections.lean:60 (same declaration text).

  5. def OAI.HarmonicArtin.ParabolicIntersections.IsAcylindrical line 31

    Also declared: ComparatorChallenges/ArtinParabolicIntersections.lean:63 (same declaration text).

  6. def OAI.HarmonicArtin.ParabolicIntersections.HasThreeOrbitLimitPoints line 36

    Also declared: ComparatorChallenges/ArtinParabolicIntersections.lean:68 (same declaration text).

  7. def OAI.HarmonicArtin.ParabolicIntersections.AcylindricallyHyperbolic line 43

    Source documentation

    An isometric non-elementary acylindrical action on a geodesic Gromov-hyperbolic metric space.

    Also declared: ComparatorChallenges/ArtinParabolicIntersections.lean:75 (same declaration text).

    def AcylindricallyHyperbolic (G : Type) [Group G] : Prop :=
…
  8. def OAI.HarmonicArtin.ParabolicIntersections.WeaklyMalnormal line 50

    Also declared: ComparatorChallenges/ArtinParabolicIntersections.lean:82 (same declaration text).

  9. def OAI.HarmonicArtin.ParabolicIntersections.IsIrreducible line 56

    Source documentation

    No nontrivial partition has every cross label equal to two.

    Also declared: ComparatorChallenges/ArtinParabolicIntersections.lean:88 (same declaration text).

    def IsIrreducible : Prop :=
…
  10. def OAI.HarmonicArtin.ParabolicIntersections.IsVisualSplit line 61

    Source documentation

    The presentation-graph condition in CMMW Definition 2.4. The vertex subgraphs are proper, cover every vertex, and omit no finite-label edge.

    def IsVisualSplit (Y Z : Set S) : Prop :=
…
  11. lemma OAI.HarmonicArtin.ParabolicIntersections.infinite_pair_visual_split line 65