OAI/Geometry/Cannon/Model.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CannonRelease.CayleyData line 10

   Also declared: ComparatorChallenges/CannonGeometricAction.lean:10 (same declaration text).

2. def OAI.CannonRelease.CayleyData.graph line 15

   Also declared: ComparatorChallenges/CannonGeometricAction.lean:15 (same declaration text).

3. def OAI.CannonRelease.CayleyData.ThinTriangles line 19

   Source documentation

   A uniform thinness constant for geodesic triangles in the Cayley graph.

   Also declared: ComparatorChallenges/CannonGeometricAction.lean:19 (same declaration text).

   def CayleyData.ThinTriangles {G : Type u} [Group G] (D : CayleyData G) : Prop :=
   …

   Mentions: OAI.CannonRelease.CayleyData

4. def OAI.CannonRelease.BasedRay line 27

   Source documentation

   Based geodesic rays, parametrized at integer times.

   Also declared: ComparatorChallenges/CannonGeometricAction.lean:27 (same declaration text).

   def BasedRay {G : Type u} [Group G] (D : CayleyData G) :=
   …

   Mentions: OAI.CannonRelease.CayleyData

5. instance OAI.CannonRelease.(instance at line 30) line 30
6. def OAI.CannonRelease.raySetoid line 35

   Source documentation

   Finite synchronous distance, equivalent to asymptoticity for based rays.

   Also declared: ComparatorChallenges/CannonGeometricAction.lean:35 (same declaration text).

   def raySetoid {G : Type u} [Group G] (D : CayleyData G) : Setoid (BasedRay D) where
   …

   Mentions: OAI.CannonRelease.CayleyData, OAI.CannonRelease.BasedRay

7. def OAI.CannonRelease.Boundary line 48

   Also declared: ComparatorChallenges/CannonGeometricAction.lean:48 (same declaration text).

8. instance OAI.CannonRelease.(instance at line 50) line 50
9. abbrev OAI.CannonRelease.SphereTwo line 54

   Also declared: ComparatorChallenges/CannonGeometricAction.lean:54 (same declaration text).

10. def OAI.CannonRelease.HyperbolicThree line 57

    Source documentation

    The upper-half-space model of hyperbolic three-space.

    Also declared: ComparatorChallenges/CannonGeometricAction.lean:57 (same declaration text).

    def HyperbolicThree := {x : Fin 3 → ℝ // 0 < x 2}

11. instance OAI.CannonRelease.(instance at line 59) line 59
12. def OAI.CannonRelease.hyperbolicDist line 62

    Also declared: ComparatorChallenges/CannonGeometricAction.lean:62 (same declaration text).

13. def OAI.CannonRelease.hyperbolicIsometries line 66

    Source documentation

    The full isometry group, including orientation-reversing isometries.

    Also declared: ComparatorChallenges/CannonGeometricAction.lean:66 (same declaration text).

    def hyperbolicIsometries : Subgroup (HyperbolicThree ≃ₜ HyperbolicThree) where
    …

    Mentions: OAI.CannonRelease.HyperbolicThree

14. abbrev OAI.CannonRelease.H3Isom line 79

    Also declared: ComparatorChallenges/CannonGeometricAction.lean:79 (same declaration text).

15. def OAI.CannonRelease.ProperAction line 81

    Also declared: ComparatorChallenges/CannonGeometricAction.lean:81 (same declaration text).

16. def OAI.CannonRelease.CocompactAction line 85

    Also declared: ComparatorChallenges/CannonGeometricAction.lean:85 (same declaration text).