OAI/Combinatorics/TreeEdit/CircleObstruction.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TreeEdit.TorusTree.branching line 10
  2. def OAI.TreeEdit.TorusTree.resolution line 11
  3. def OAI.TreeEdit.TorusTree.cutoff line 12
  4. def OAI.TreeEdit.TorusTree.repetitions line 13
  5. def OAI.TreeEdit.TorusTree.Pool line 14
  6. instance OAI.TreeEdit.TorusTree.poolFintype line 15
  7. def OAI.TreeEdit.TorusTree.poolPrime line 16
  8. def OAI.TreeEdit.TorusTree.residueModulus line 17
  9. lemma OAI.TreeEdit.TorusTree.pool_properties line 19
  10. lemma OAI.TreeEdit.TorusTree.residueModulus_pos line 22
  11. instance OAI.TreeEdit.TorusTree.residueModulus_neZero line 25
  12. lemma OAI.TreeEdit.TorusTree.parameter_spacing line 27
  13. lemma OAI.TreeEdit.TorusTree.probability_error_eventually line 43
  14. lemma OAI.TreeEdit.TorusTree.torus_parameters_eventually line 69
  15. lemma OAI.TreeEdit.TorusTree.good_halfturn_eventually line 106
  16. def OAI.TreeEdit.TorusTree.allPeriods line 135
  17. lemma OAI.TreeEdit.TorusTree.allPeriods_pos line 138
  18. def OAI.TreeEdit.TorusTree.fineModulus line 141
  19. lemma OAI.TreeEdit.TorusTree.fine_parameters line 144
  20. lemma OAI.TreeEdit.TorusTree.period_upper line 167
  21. lemma OAI.TreeEdit.TorusTree.spectrum_error line 173
  22. theorem OAI.TreeEdit.TorusTree.concrete_displacement line 196
  23. lemma OAI.TreeEdit.TorusTree.sampled_separation line 214