OAI/Computability/DirectedFeedback/Games/Game.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.event_nonempty line 14
2. def OAI.DFVSGames.Foundations.Hastad.SourceGame.eventLaw line 18
3. def OAI.DFVSGames.Foundations.Hastad.SourceGame.visibleQuestion line 23
4. def OAI.DFVSGames.Foundations.Hastad.SourceGame.baseGame line 27
5. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.baseGame_accepts line 32
6. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.eventLaw_probability line 36
7. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.sum_slots line 49
8. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.sum_slot_accepts line 59
9. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.failureCount_eq_sum_map line 73
10. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.failureCount_allIndices line 81
11. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.verifier_probability_plus_failure line 88
12. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.base_success_le_verifier line 109
13. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.base_value_le_of_clause_gap line 119
14. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.pushforward_comp line 139
15. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.expectation_pushforward line 154
16. def OAI.DFVSGames.Foundations.Hastad.SourceGame.repeatedVisible line 165
17. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.repeated_questions line 170
18. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.repeated_expectation line 179
19. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.repeated_expectation_split line 190
20. def OAI.DFVSGames.Foundations.Hastad.SourceGame.sourceProjectionGame line 204
21. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.projection_value_le_repetition line 209
22. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.source_acceptance_le line 228
23. theorem OAI.DFVSGames.Foundations.Hastad.SourceGame.source_acceptance_le_split line 243
24. def OAI.DFVSGames.Foundations.Hastad.SourceSoundness.leftTable line 271
25. def OAI.DFVSGames.Foundations.Hastad.SourceSoundness.rightOracle line 275
26. theorem OAI.DFVSGames.Foundations.Hastad.SourceSoundness.rightOracle_answer line 283
27. theorem OAI.DFVSGames.Foundations.Hastad.SourceSoundness.leftTable_answer line 289
28. theorem OAI.DFVSGames.Foundations.Hastad.SourceSoundness.sourceList_sound line 293
29. theorem OAI.DFVSGames.Foundations.Hastad.SourceSoundness.sourceList_sound_rat line 311
30. def OAI.DFVSGames.Foundations.Hastad.SourceHonest.taggedAssignment line 335
31. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.taggedAssignment_left line 341
32. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.taggedAssignment_right line 345
33. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.taggedAssignment_right_restriction line 349
34. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.conditioned_equation_honest_satisfied line 366
35. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.mapped_conditioned_equation_honest_satisfied line 378
36. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.tapeAcceptance_conditioned_dictators line 397
37. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.numbered_assignment_restriction line 415
38. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.conditionedOccurrence_honest_satisfied line 436
39. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.conditionedOccurrenceList_honest_acceptance line 449
40. def OAI.DFVSGames.Foundations.Hastad.SourceHonest.honestGlobal line 482
41. def OAI.DFVSGames.Foundations.Hastad.SourceHonest.honestBits line 488
42. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.honestBits_code line 493
43. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.honestBits_dummy line 501
44. def OAI.DFVSGames.Foundations.Hastad.SourceHonest.honestValidJ line 507
45. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.validJ_nonempty_of_satisfying line 513
46. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.leftResponse_honest line 519
47. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.rightResponse_honest line 527
48. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.context_tapeAcceptance line 550
49. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.sourceEquation_honest_satisfied line 564
50. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.rawSourceList_honest_acceptance line 574
51. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_nonempty line 593
52. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance line 603
53. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_rat line 617
54. theorem OAI.DFVSGames.Foundations.Hastad.SourceHonest.sourceList_honest_acceptance_nonempty_rat line 627
55. def OAI.DFVSGames.Foundations.Repetition.logTwo line 644
56. theorem OAI.DFVSGames.Foundations.Repetition.logTwo_one line 646
57. theorem OAI.DFVSGames.Foundations.Repetition.logTwo_inv_le_of_half_pow_le line 648
58. theorem OAI.DFVSGames.Foundations.Repetition.contraction_step line 660
59. theorem OAI.DFVSGames.Foundations.Repetition.initial_step line 699
60. theorem OAI.DFVSGames.Foundations.Repetition.cutoff_step line 704
61. theorem OAI.DFVSGames.Foundations.Repetition.cutoff_le_length line 716
62. def OAI.DFVSGames.Foundations.Repetition.ScalarRecurrence line 724
63. theorem OAI.DFVSGames.Foundations.Repetition.decay_to_cutoff line 728
64. theorem OAI.DFVSGames.Foundations.Repetition.block_contraction line 765
65. theorem OAI.DFVSGames.Foundations.Repetition.scalar_bound_6000 line 777
66. def OAI.DFVSGames.Foundations.Repetition.incidenceRate line 800
67. theorem OAI.DFVSGames.Foundations.Repetition.incidenceRate_pos line 802
68. theorem OAI.DFVSGames.Foundations.Repetition.incidenceRate_lt_one line 804
69. theorem OAI.DFVSGames.Foundations.Repetition.incidenceRate_fourth line 806
70. theorem OAI.DFVSGames.Foundations.Repetition.incidence_rate_comparison line 810
71. theorem OAI.DFVSGames.Foundations.Repetition.scalar_incidence_bound line 821