OAI/Computability/DirectedFeedback/Games/Parameters.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Integration.SourceParameters.rate line 9
2. theorem OAI.DFVSGames.Integration.SourceParameters.rate_bounds line 11
3. theorem OAI.DFVSGames.Integration.SourceParameters.fourth_power_comparison line 17
4. theorem OAI.DFVSGames.Integration.SourceParameters.four_bit_rate_comparison line 33
5. theorem OAI.DFVSGames.Integration.SourceParameters.logTwo_sixteen line 48
6. theorem OAI.DFVSGames.Integration.SourceParameters.game_repetition_rate line 54
7. def OAI.DFVSGames.Integration.SourceParameters.sourceThreshold line 72
8. theorem OAI.DFVSGames.Integration.SourceParameters.sourceThreshold_pos line 74
9. theorem OAI.DFVSGames.Integration.SourceParameters.exists_repetition_length line 79
10. def OAI.DFVSGames.Integration.SourceParameters.repetitionLength line 85
11. theorem OAI.DFVSGames.Integration.SourceParameters.repetitionLength_spec line 89
12. theorem OAI.DFVSGames.Integration.SourceParameters.repetitionLength_real_bound line 95
13. def OAI.DFVSGames.Foundations.Hastad.SourceGap.ClauseGap line 113
14. theorem OAI.DFVSGames.Foundations.Hastad.SourceGap.third_pos line 118
15. theorem OAI.DFVSGames.Foundations.Hastad.SourceGap.third_le_one line 120
16. def OAI.DFVSGames.Foundations.Hastad.SourceGap.repetitionCount line 122
17. theorem OAI.DFVSGames.Foundations.Hastad.SourceGap.repetitionCount_pos line 126
18. theorem OAI.DFVSGames.Foundations.Hastad.SourceGap.repeated_game_bound line 131
19. def OAI.DFVSGames.Foundations.Hastad.SourceGap.source line 147
20. theorem OAI.DFVSGames.Foundations.Hastad.SourceGap.source_complete line 151
21. theorem OAI.DFVSGames.Foundations.Hastad.SourceGap.source_sound line 164
22. theorem OAI.DFVSGames.Foundations.Hastad.SourceGap.source_size line 175
23. def OAI.DFVSGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator line 186
24. theorem OAI.DFVSGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_ge_two line 188
25. theorem OAI.DFVSGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_pos line 192
26. theorem OAI.DFVSGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_inv_pos line 195
27. theorem OAI.DFVSGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_inv_le_half line 200
28. theorem OAI.DFVSGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_inv_le line 206
29. def OAI.DFVSGames.Foundations.Hastad.SourceGap.forError line 229
30. theorem OAI.DFVSGames.Foundations.Hastad.SourceGap.forError_complete line 233
31. theorem OAI.DFVSGames.Foundations.Hastad.SourceGap.forError_sound line 242
32. theorem OAI.DFVSGames.Foundations.Hastad.SourceGap.forError_size line 251
33. abbrev OAI.DFVSGames.Foundations.Hastad.SourceGeneratorContract.NonemptyFormula line 263
34. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorContract.inputEncoding line 265
35. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorContract.sourceMap line 267
36. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorContract.errorMap line 271
37. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorContract.inputEncoding_mk line 275
38. abbrev OAI.DFVSGames.Foundations.Hastad.SourceGeneratorProgram.Tape line 286
39. abbrev OAI.DFVSGames.Foundations.Hastad.SourceGeneratorProgram.Ambient line 287
40. abbrev OAI.DFVSGames.Foundations.Hastad.SourceGeneratorProgram.State line 288
41. inductive OAI.DFVSGames.Foundations.Hastad.SourceGeneratorProgram.Label line 292
42. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorProgram.bodyEntry line 301
43. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorProgram.next line 303
44. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorProgram.sourceStateEquiv line 306
45. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorProgram.program line 312
46. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorProgram.main line 329
47. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorProgram.machine line 331
48. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorProgram.finite_work_alphabets line 342
49. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorProgram.atCheck line 347
50. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorProgram.atReset line 351
51. theorem OAI.DFVSGames.Foundations.Hastad.SourceGenerator.source_initial line 367
52. theorem OAI.DFVSGames.Foundations.Hastad.SourceGenerator.initial_configuration line 371
53. def OAI.DFVSGames.Foundations.Hastad.SourceGenerator.startupInTime line 384
54. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.clauseRank_le_power line 410
55. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.variableRank_le_power line 416
56. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.leftValue_le_numberBound line 423
57. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.rightValue_le_numberBound line 429
58. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.leftBlock_le_numberBound line 434
59. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.rankPolynomial line 442
60. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.numberPolynomial line 443
61. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.rankPolynomial_eval line 446
62. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.numberPolynomial_eval line 448
63. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.slotPolynomial line 452
64. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.slotPolynomial_eval line 459
65. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.slotBudget_le line 468
66. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.prefixBudget_le line 487
67. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.preparePolynomial line 501
68. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.preparePolynomial_eval line 506
69. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.setupPolynomial line 513
70. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.setupPolynomial_eval line 519
71. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.finishPolynomial line 527
72. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.finishPolynomial_eval line 531
73. def OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.bodyPolynomial line 537
74. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.setupBudget_le line 540
75. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.finishBudget_le line 557
76. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.bodyBudget_le line 564
77. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.fixed_parameters_body_bound line 573
78. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleBound.bodyInPolynomialTime line 578
79. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.accumulatorRole line 607
80. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.leafTapes line 610
81. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.leaf_accumulator line 615
82. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.leaf_work_blank line 619
83. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.leaf_ready line 628
84. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.body_result_leaf line 655
85. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.source_initial line 665
86. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.actual_bodies line 669
87. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.resetDigits_ready line 692
88. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.allBits_eq_records line 698
89. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.accumulated_eq_input line 709
90. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.traversalOutput line 721
91. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.traversalOutput_accumulator line 725
92. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.traversalOutput_frame line 730
93. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.resetLabel line 735
94. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.traversalInTime line 738
95. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.timePolynomial line 782
96. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorTraversal.traversalInPolynomialTime line 785