OAI/Computability/MinUncut/PCP/SelectionSequence.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncutGames.Foundations.Repetition.SelectionSequence.exists_unused line 9
  2. def OAI.MinUncutGames.Foundations.Repetition.SelectionSequence.nextSet line 25
  3. def OAI.MinUncutGames.Foundations.Repetition.SelectionSequence.selectedSet line 31
  4. theorem OAI.MinUncutGames.Foundations.Repetition.SelectionSequence.selectedSet_card line 37
  5. theorem OAI.MinUncutGames.Foundations.Repetition.SelectionSequence.selectedSet_subset_succ line 60
  6. theorem OAI.MinUncutGames.Foundations.Repetition.SelectionSequence.selectedSet_monotone line 70
  7. theorem OAI.MinUncutGames.Foundations.Repetition.SelectionSequence.selectedSet_univ line 76
  8. theorem OAI.MinUncutGames.Foundations.Repetition.SelectionSequence.selectedSet_step line 83
  9. def OAI.MinUncutGames.Foundations.Repetition.SelectionSequence.SetStep line 98
  10. theorem OAI.MinUncutGames.Foundations.Repetition.SelectionSequence.totalSetStep line 104
  11. theorem OAI.MinUncutGames.Foundations.Repetition.SelectionSequence.exists_scalar_sequence line 119
  12. def OAI.MinUncutGames.Foundations.Repetition.SelectionSequence.ConditionalCoordinateBound line 152
  13. theorem OAI.MinUncutGames.Foundations.Repetition.SelectionSequence.repetition_success_le_of_conditionalCoordinateBound line 164
  14. theorem OAI.MinUncutGames.Foundations.Repetition.selected_coordinate_probability_le_value_add_error line 201
  15. theorem OAI.MinUncutGames.Foundations.Repetition.holenstein_conditionalCoordinateBound line 230
  16. theorem OAI.MinUncutGames.Foundations.Repetition.holenstein_repetition_success line 244
  17. theorem OAI.MinUncutGames.Foundations.Repetition.holenstein_repetition_value line 254
  18. def OAI.MinUncut.Outer.repetitionRate line 271
  19. lemma OAI.MinUncut.Outer.repetitionRate_pos line 272
  20. lemma OAI.MinUncut.Outer.repetitionRate_lt_one line 273
  21. lemma OAI.MinUncut.Outer.repetitionRate_fourth line 274
  22. lemma OAI.MinUncut.Outer.ordinary_alphabet_log line 277
  23. theorem OAI.MinUncut.Outer.ordinary_repetition_success line 287