OAI/Computability/DirectedFeedback/Machines/Tape.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Hastad.SourceTape.TestTape line 14
2. abbrev OAI.DFVSGames.Foundations.Hastad.SourceTape.FairTestTape line 17
3. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.expect_prod line 23
4. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.card_testTape line 34
5. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.card_fairTestTape line 39
6. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.expect_testTape line 45
7. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.expect_equivTape line 53
8. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.expect_fairTestTape line 58
9. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.expect_fairTestTape_ignore line 67
10. def OAI.DFVSGames.Foundations.Hastad.SourceTape.tapeQueries line 72
11. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.expect_tapeQueries line 75
12. def OAI.DFVSGames.Foundations.Hastad.SourceTape.tapeAcceptance line 86
13. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_realizedTestAcceptance line 92
14. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_testAcceptance line 97
15. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.tapeAcceptance_eq_sum_div_card line 103
16. def OAI.DFVSGames.Foundations.Hastad.SourceTape.restrictFunction line 116
17. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.expect_restrictFunction line 119
18. def OAI.DFVSGames.Foundations.Hastad.SourceTape.restrictTape line 134
19. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.expect_restrictTape line 138
20. def OAI.DFVSGames.Foundations.Hastad.SourceTape.restrictedProjection line 166
21. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.restrict_realizedNoise line 170
22. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.restrict_thirdQuery line 173
23. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.expect_restricted_queries line 179
24. def OAI.DFVSGames.Foundations.Hastad.SourceTape.restrictRightTape line 191
25. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.expect_restrictRightTape line 195
26. theorem OAI.DFVSGames.Foundations.Hastad.SourceTape.expect_rightRestricted_queries line 214
27. def OAI.DFVSGames.Foundations.Hastad.SourceContexts.clauseAnswerEquiv line 236
28. def OAI.DFVSGames.Foundations.Hastad.SourceContexts.clauseAnswerFinEquiv line 242
29. instance OAI.DFVSGames.Foundations.Hastad.SourceContexts.clauseAnswerFintype line 248
30. instance OAI.DFVSGames.Foundations.Hastad.SourceContexts.clauseAnswerInhabited line 251
31. instance OAI.DFVSGames.Foundations.Hastad.SourceContexts.slotFintype line 253
32. instance OAI.DFVSGames.Foundations.Hastad.SourceContexts.slotInhabited line 257
33. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.card_clauseAnswer line 259
34. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.card_slot line 263
35. abbrev OAI.DFVSGames.Foundations.Hastad.SourceContexts.I line 265
36. abbrev OAI.DFVSGames.Foundations.Hastad.SourceContexts.J line 266
37. abbrev OAI.DFVSGames.Foundations.Hastad.SourceContexts.ClauseContext line 267
38. abbrev OAI.DFVSGames.Foundations.Hastad.SourceContexts.VariableContext line 268
39. abbrev OAI.DFVSGames.Foundations.Hastad.SourceContexts.SlotContext line 269
40. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.card_I line 271
41. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.card_J line 272
42. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.card_ClauseContext line 273
43. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.card_VariableContext line 275
44. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.card_SlotContext line 277
45. def OAI.DFVSGames.Foundations.Hastad.SourceContexts.localConsistent line 280
46. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.localConsistent_eq_true_iff line 284
47. def OAI.DFVSGames.Foundations.Hastad.SourceContexts.validJ line 291
48. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.validJ_eq_true_iff line 296
49. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.validJ_satisfies line 304
50. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.validJ_consistent line 309
51. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.validJ_localConsistent line 316
52. def OAI.DFVSGames.Foundations.Hastad.SourceContexts.canonicalSlot line 323
53. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.canonicalSlot_name line 327
54. def OAI.DFVSGames.Foundations.Hastad.SourceContexts.pi line 339
55. def OAI.DFVSGames.Foundations.Hastad.SourceContexts.sampledVariables line 343
56. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.sampledVariables_supported line 347
57. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.sampled_eq_pi line 352
58. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.sampled_answers_eq_of_visible_eq line 360
59. def OAI.DFVSGames.Foundations.Hastad.SourceContexts.honestJ line 368
60. def OAI.DFVSGames.Foundations.Hastad.SourceContexts.honestI line 372
61. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.honestJ_valid line 376
62. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.pi_honest line 388
63. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.pi_honest_sampled line 396
64. def OAI.DFVSGames.Foundations.Hastad.SourceContexts.baseAccepts line 402
65. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.baseAccepts_eq_true_iff line 408
66. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.projection_implies_coordinate_accepts line 416
67. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.baseAccepts_implies_sampled line 423
68. theorem OAI.DFVSGames.Foundations.Hastad.SourceContexts.projection_implies_sampled_accepts line 433
69. structure OAI.DFVSGames.Reduction.SourceEncoding.Input line 449
70. abbrev OAI.DFVSGames.Reduction.SourceEncoding.Table line 454
71. def OAI.DFVSGames.Reduction.SourceEncoding.equationWords line 456
72. def OAI.DFVSGames.Reduction.SourceEncoding.inputWords line 459
73. def OAI.DFVSGames.Reduction.SourceEncoding.inputBits line 462
74. def OAI.DFVSGames.Reduction.SourceEncoding.parseEquation line 464
75. theorem OAI.DFVSGames.Reduction.SourceEncoding.parseEquation_encoded line 480
76. def OAI.DFVSGames.Reduction.SourceEncoding.parseEquations line 487
77. theorem OAI.DFVSGames.Reduction.SourceEncoding.parseEquations_encoded line 495
78. def OAI.DFVSGames.Reduction.SourceEncoding.decodeInputWords line 504
79. theorem OAI.DFVSGames.Reduction.SourceEncoding.decodeInputWords_encoded line 514
80. def OAI.DFVSGames.Reduction.SourceEncoding.decodeInputBits line 523
81. theorem OAI.DFVSGames.Reduction.SourceEncoding.decodeInputBits_encoded line 526
82. theorem OAI.DFVSGames.Reduction.SourceEncoding.inputWords_injective line 530
83. theorem OAI.DFVSGames.Reduction.SourceEncoding.inputBits_injective line 535
84. theorem OAI.DFVSGames.Reduction.SourceEncoding.equationWords_length line 540
85. theorem OAI.DFVSGames.Reduction.SourceEncoding.equationsWords_length line 543
86. theorem OAI.DFVSGames.Reduction.SourceEncoding.inputWords_length line 552
87. theorem OAI.DFVSGames.Reduction.SourceEncoding.equationBits_length_le line 557
88. theorem OAI.DFVSGames.Reduction.SourceEncoding.equationsBits_length_le line 564
89. theorem OAI.DFVSGames.Reduction.SourceEncoding.inputBits_length line 575
90. theorem OAI.DFVSGames.Reduction.SourceEncoding.inputBits_length_le line 582
91. theorem OAI.DFVSGames.Reduction.SourceEncoding.inputBits_length_ge_variables line 588
92. theorem OAI.DFVSGames.Reduction.SourceEncoding.inputBits_length_ge_equations line 591