OAI/Geometry/HyperbolicGroups/SamplingStage.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.Alphabet line 16
  2. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.Matches line 17
  3. instance OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.(instance at line 18) line 18
  4. def OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.label line 20
  5. lemma OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.size_tendsto line 22
  6. theorem OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.samplingSequence line 27

    Source documentation

    The genuine pure combinatorial sampling sequence, obtained by diagonalizing actual finite table realizations. The laws in its conclusion are not hypotheses.

    theorem samplingSequence : SamplingSequence Field Admissible (Alphabet s) (Matches s) (label s) where
…

    Mentions: OAI.HyperbolicObstruction.SamplingSequence, OAI.HyperbolicObstruction.IncidenceTemplate.Field, OAI.HyperbolicObstruction.IncidenceTemplate.Admissible, OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.Alphabet, OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.Matches, OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.label

  7. def OAI.HyperbolicObstruction.IncidenceTemplate.samplingParameter line 46

    Source documentation

    One admissible positive parameter sequence. Later diagram restrictions may be imposed by choosing smaller parameters before each finite selection.

    def samplingParameter (m : ℕ) : ℝ := 1 / (1000*(m+1:ℝ))
  8. lemma OAI.HyperbolicObstruction.IncidenceTemplate.samplingParameter_pos line 47
  9. lemma OAI.HyperbolicObstruction.IncidenceTemplate.samplingParameter_lt_one line 48
  10. lemma OAI.HyperbolicObstruction.IncidenceTemplate.samplingParameter_small line 52
  11. lemma OAI.HyperbolicObstruction.IncidenceTemplate.samplingParameter_tendsto line 57
  12. def OAI.HyperbolicObstruction.IncidenceTemplate.actualSamplingStage line 66
  13. theorem OAI.HyperbolicObstruction.IncidenceTemplate.actualSamplingSequence line 72

    Source documentation

    An unconditional table sampling producer. Asphericity and filling still require the separate diagram event on these same tables.

    theorem actualSamplingSequence : SamplingSequence Field Admissible
    (SamplingStage.Alphabet actualSamplingStage) (SamplingStage.Matches actualSamplingStage)
    (SamplingStage.label actualSamplingStage) := SamplingStage.samplingSequence actualSamplingStage
…

    Mentions: OAI.HyperbolicObstruction.SamplingSequence, OAI.HyperbolicObstruction.IncidenceTemplate.Field, OAI.HyperbolicObstruction.IncidenceTemplate.Admissible, OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.Alphabet, OAI.HyperbolicObstruction.IncidenceTemplate.actualSamplingStage, OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.Matches, OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.label, OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.samplingSequence