OAI/Geometry/HyperbolicGroups/Test.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest line 18

   Source documentation

   A literal conditional test of Section 4, with k+1 branches.

   structure ConditionalTest where
   …

2. def OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest.closure line 27
3. lemma OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest.closure_spec line 30
4. lemma OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest.closure_gap line 36
5. def OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest.threshold line 41
6. def OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest.rate line 44
7. lemma OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest.rate_tendsto line 47
8. def OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest.embedding line 52
9. def OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest.error line 57
10. lemma OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest.error_nonneg line 62
11. lemma OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest.expectedError line 66
12. def OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest.Satisfies line 76

    Source documentation

    The coupling is on actual master matches. Its branches agree on exactly the prescribed named fields, with no assumptions about numerical cross-field values.

    def Satisfies (t : ConditionalTest) (w : TableModel.Entry (A := A) rowSupport → Bool) (η : ℝ) : Prop :=
    …

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest, OAI.HyperbolicObstruction.TableModel.Entry, OAI.HyperbolicObstruction.IncidenceTemplate.rowSupport

13. lemma OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest.satisfies_of_error line 83