OAI/Geometry/HyperbolicGroups/SelectedPresentation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.LetterGroup line 19
2. def OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.letter line 21
3. def OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.inverse line 24
4. lemma OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.letter_inverse line 27
5. lemma OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.letter_generates line 31
6. def OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.potential line 34
7. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.Rows line 37
8. instance OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.(instance at line 38) line 38
9. def OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.rowLaw line 41
10. def OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.row line 43
11. lemma OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.row_relation line 46
12. lemma OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.marginal line 50
13. theorem OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.eventually_noAction line 58

    Source documentation

    Concrete no-action conclusion for the literal random letter presentations, provided the still-missing diagram argument proves those same groups infinite. The sampling laws, relator potentials, row relations and marginals are proved, not supplied by this hypothesis.

    theorem eventually_noAction [∀ m, Infinite (LetterGroup s m)] :
        ∀ᶠ m in atTop, NoGeometricCATZeroAction (LetterGroup s m) :=
    …

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.LetterGroup, OAI.HyperbolicObstruction.NoGeometricCATZeroAction