OAI/Computability/DegreeRigidity/OrdinalCodes/Recurrence.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.choiceBit line 14
  2. def OAI.TuringRigidity.state line 16
  3. def OAI.TuringRigidity.branch line 20
  4. theorem OAI.TuringRigidity.choiceBit_eq_zero_or_one line 23
  5. theorem OAI.TuringRigidity.state_mem_Icc line 28
  6. theorem OAI.TuringRigidity.state_eq_sum line 58
  7. theorem OAI.TuringRigidity.frequency_error line 68
  8. def OAI.TuringRigidity.rationalSpan line 81
  9. theorem OAI.TuringRigidity.rationalSpan_countable line 83
  10. theorem OAI.TuringRigidity.state_mem_rationalSpan line 91
  11. theorem OAI.TuringRigidity.state_mem_Icc_on_span line 112
  12. theorem OAI.TuringRigidity.exists_radius_lt line 143
  13. theorem OAI.TuringRigidity.comparison_search line 153
  14. theorem OAI.TuringRigidity.irrational_cut_iff_search line 175