OAI/Geometry/HyperbolicGroups/DiagonalSampling.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.IncidenceTemplate.stageError line 16
2. lemma OAI.HyperbolicObstruction.IncidenceTemplate.stageError_pos line 17
3. lemma OAI.HyperbolicObstruction.IncidenceTemplate.stageError_le_third line 18
4. lemma OAI.HyperbolicObstruction.IncidenceTemplate.stageError_tendsto line 22
5. structure OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage line 31

   Source documentation

   All finitely many requested tests and the actual six-letter array at one stage. This is selected below, not an assumption about a desired action.

   structure SamplingStage (m : ℕ) (δ : ℝ) where
   …

6. lemma OAI.HyperbolicObstruction.IncidenceTemplate.exists_samplingStage line 40