OAI/Computability/PerfectCompleteness/Repetition/RepetitionRateLemmas.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.RepetitionRate.halfRate line 15
  2. theorem OAI.PerfectCompleteness.RepetitionRate.halfRate_bounds line 17
  3. theorem OAI.PerfectCompleteness.RepetitionRate.halfRate_cast line 26
  4. theorem OAI.PerfectCompleteness.RepetitionRate.halfRate_power_comparison line 31
  5. theorem OAI.PerfectCompleteness.RepetitionRate.halfRate_rpow_comparison line 50
  6. theorem OAI.PerfectCompleteness.RepetitionRate.game_repetition_halfRate line 65
  7. theorem OAI.PerfectCompleteness.RepetitionRate.occurrence_repetition_halfRate line 81
  8. def OAI.PerfectCompleteness.RepetitionRate.bernoulli line 97
  9. def OAI.PerfectCompleteness.RepetitionRate.cleanCount line 105
  10. theorem OAI.PerfectCompleteness.RepetitionRate.pow_cleanCount_eq_prod line 108
  11. theorem OAI.PerfectCompleteness.RepetitionRate.cleanMask_moment line 113
  12. theorem OAI.PerfectCompleteness.RepetitionRate.cube_decay_bound line 127
  13. theorem OAI.PerfectCompleteness.RepetitionRate.exists_cube_decay_lt line 147
  14. theorem OAI.PerfectCompleteness.RepetitionRate.exists_clean_branching line 160
  15. def OAI.PerfectCompleteness.IndexedRepetition.game line 186
  16. def OAI.PerfectCompleteness.IndexedRepetition.reindexStrategy line 196
  17. theorem OAI.PerfectCompleteness.IndexedRepetition.law_const_fin line 202
  18. theorem OAI.PerfectCompleteness.IndexedRepetition.game_fin line 208
  19. theorem OAI.PerfectCompleteness.IndexedRepetition.reindex_law line 217
  20. theorem OAI.PerfectCompleteness.IndexedRepetition.reindex_success line 224
  21. theorem OAI.PerfectCompleteness.IndexedRepetition.success_le_repetition_value line 255
  22. theorem OAI.PerfectCompleteness.IndexedRepetition.value_eq_repetition line 263
  23. theorem OAI.PerfectCompleteness.IndexedRepetition.halfRate line 275