OAI/Combinatorics/IndependentSets/Machines/Tape.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.TestTape line 14
  2. abbrev OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.FairTestTape line 17
  3. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.expect_prod line 23
  4. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.card_testTape line 34
  5. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.card_fairTestTape line 39
  6. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.expect_testTape line 45
  7. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.expect_equivTape line 53
  8. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.expect_fairTestTape line 58
  9. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.expect_fairTestTape_ignore line 67
  10. def OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.tapeQueries line 72
  11. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.expect_tapeQueries line 75
  12. def OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.tapeAcceptance line 86
  13. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_realizedTestAcceptance line 92
  14. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_testAcceptance line 97
  15. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_sum_div_card line 103
  16. def OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.restrictFunction line 115
  17. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.expect_restrictFunction line 118
  18. def OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.restrictTape line 133
  19. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.expect_restrictTape line 137
  20. def OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.restrictedProjection line 165
  21. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.restrict_realizedNoise line 169
  22. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.restrict_thirdQuery line 172
  23. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.expect_restricted_queries line 178
  24. def OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.restrictRightTape line 190
  25. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.expect_restrictRightTape line 194
  26. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceTape.expect_rightRestricted_queries line 213