OAI/Geometry/HyperbolicGroups/FiniteSampling.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest.satisfies_mono line 18
2. theorem OAI.HyperbolicObstruction.IncidenceTemplate.eventually_exists_tables_precision line 26

   Source documentation

   The sampling conclusions at any requested positive accuracy are realized on all sufficiently large signed alphabets, after fixing the parameters.

   theorem eventually_exists_tables_precision {J : Type*} [Fintype J]
       (T : J → ConditionalTest) {α β δ ξ τ : ℝ}
       (ha : 0 ≤ α) (hb : 7*α ≤ β) (hd : 0 ≤ δ) (hd1 : δ < 1)
       (hsmall : ∀ j, ((T j).k+1:ℝ)*(β+90*δ) ≤ 1/2)
       (hξ : 0 < ξ) (hτ0 : 0 < τ) (hτ2 : τ ≤ 2) :
       ∀ᶠ n in atTop, ∃ (w : TableModel.Entry (A := SymmetricAlphabet n) rowSupport → Bool)
   …

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

3. lemma OAI.HyperbolicObstruction.IncidenceTemplate.admissible_singleton line 56
4. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalData line 73

   Source documentation

   The finite named-field part of a conditional test.

   abbrev ConditionalData := {p : Finset Field × Field // p.2 ∉ p.1 ∧ Admissible (insert p.2 p.1)}

   Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Field, OAI.HyperbolicObstruction.IncidenceTemplate.Admissible

5. instance OAI.HyperbolicObstruction.IncidenceTemplate.(instance at line 74) line 74
6. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalData.test line 76
7. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.singletonData line 79
8. lemma OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest.singleton_bound line 82