OAI/Computability/BinPacking/Information/GameDecoder.lean

GitHub source file

152 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Hastad.Cube line 24
2. def OAI.BinPackingGames.Foundations.Hastad.bitSign line 26
3. theorem OAI.BinPackingGames.Foundations.Hastad.bitSign_sq line 28
4. theorem OAI.BinPackingGames.Foundations.Hastad.bitSign_xor line 31
5. def OAI.BinPackingGames.Foundations.Hastad.cubeXor line 35
6. def OAI.BinPackingGames.Foundations.Hastad.walsh line 37
7. theorem OAI.BinPackingGames.Foundations.Hastad.walsh_symm line 40
8. theorem OAI.BinPackingGames.Foundations.Hastad.walsh_sq line 44
9. theorem OAI.BinPackingGames.Foundations.Hastad.walsh_xor line 48
10. theorem OAI.BinPackingGames.Foundations.Hastad.coordinate_orthogonality line 56
11. theorem OAI.BinPackingGames.Foundations.Hastad.walsh_sum_orthogonality line 61
12. theorem OAI.BinPackingGames.Foundations.Hastad.walsh_orthogonality line 78
13. def OAI.BinPackingGames.Foundations.Hastad.coefficient line 85
14. theorem OAI.BinPackingGames.Foundations.Hastad.walsh_inversion line 88
15. theorem OAI.BinPackingGames.Foundations.Hastad.walsh_inner line 105
16. theorem OAI.BinPackingGames.Foundations.Hastad.walsh_parseval line 122
17. theorem OAI.BinPackingGames.Foundations.Hastad.sign_parseval line 126
18. def OAI.BinPackingGames.Foundations.Hastad.support line 136
19. def OAI.BinPackingGames.Foundations.Hastad.noiseWeight line 138
20. theorem OAI.BinPackingGames.Foundations.Hastad.noiseWeight_nonneg line 142
21. theorem OAI.BinPackingGames.Foundations.Hastad.noiseWeight_sum line 148
22. theorem OAI.BinPackingGames.Foundations.Hastad.noise_walsh line 153
23. def OAI.BinPackingGames.Foundations.Hastad.thirdQuery line 166
24. theorem OAI.BinPackingGames.Foundations.Hastad.walsh_autocorrelation line 169
25. def OAI.BinPackingGames.Foundations.Hastad.projectedCoefficient line 187
26. def OAI.BinPackingGames.Foundations.Hastad.testBias line 190
27. theorem OAI.BinPackingGames.Foundations.Hastad.testBias_fourier line 194
28. def OAI.BinPackingGames.Foundations.Hastad.testAcceptance line 222
29. theorem OAI.BinPackingGames.Foundations.Hastad.threeBit_indicator line 227
30. theorem OAI.BinPackingGames.Foundations.Hastad.testAcceptance_eq line 232
31. def OAI.BinPackingGames.Foundations.Hastad.cubeFlip line 260
32. theorem OAI.BinPackingGames.Foundations.Hastad.cubeFlip_cubeFlip line 263
33. theorem OAI.BinPackingGames.Foundations.Hastad.bitSign_not line 267
34. theorem OAI.BinPackingGames.Foundations.Hastad.sum_cubeFlip line 270
35. theorem OAI.BinPackingGames.Foundations.Hastad.coefficient_zero_of_odd line 282
36. theorem OAI.BinPackingGames.Foundations.Hastad.coefficient_sign_zero_of_folded line 291
37. def OAI.BinPackingGames.Foundations.Hastad.representative line 298
38. theorem OAI.BinPackingGames.Foundations.Hastad.representative_at line 302
39. theorem OAI.BinPackingGames.Foundations.Hastad.representative_flip line 307
40. abbrev OAI.BinPackingGames.Foundations.Hastad.HalfCube line 311
41. def OAI.BinPackingGames.Foundations.Hastad.canonicalInput line 313
42. theorem OAI.BinPackingGames.Foundations.Hastad.canonicalInput_flip line 317
43. def OAI.BinPackingGames.Foundations.Hastad.foldedAnswer line 322
44. theorem OAI.BinPackingGames.Foundations.Hastad.foldedAnswer_flip line 326
45. theorem OAI.BinPackingGames.Foundations.Hastad.foldedAnswer_zero_coefficient line 334
46. theorem OAI.BinPackingGames.Foundations.Hastad.foldedAnswer_dictator line 339
47. def OAI.BinPackingGames.Foundations.Hastad.coordinateMask line 344
48. def OAI.BinPackingGames.Foundations.Hastad.cubeToggle line 346
49. theorem OAI.BinPackingGames.Foundations.Hastad.cubeToggle_twice line 350
50. theorem OAI.BinPackingGames.Foundations.Hastad.walsh_coordinateMask line 356
51. theorem OAI.BinPackingGames.Foundations.Hastad.walsh_cubeToggle line 366
52. theorem OAI.BinPackingGames.Foundations.Hastad.sum_cubeToggle line 371
53. def OAI.BinPackingGames.Foundations.Hastad.restrictQuery line 384
54. theorem OAI.BinPackingGames.Foundations.Hastad.restrictQuery_cubeToggle line 388
55. theorem OAI.BinPackingGames.Foundations.Hastad.conditioned_coefficient_zero_invalid line 399
56. theorem OAI.BinPackingGames.Foundations.Hastad.conditioned_coefficient_support line 409
57. def OAI.BinPackingGames.Foundations.Hastad.conditionedFoldedAnswer line 419
58. theorem OAI.BinPackingGames.Foundations.Hastad.conditionedFoldedAnswer_flip line 424
59. theorem OAI.BinPackingGames.Foundations.Hastad.conditionedFoldedAnswer_zero_coefficient line 431
60. theorem OAI.BinPackingGames.Foundations.Hastad.conditionedFoldedAnswer_dictator line 438
61. def OAI.BinPackingGames.Foundations.Hastad.parityProjection line 450
62. theorem OAI.BinPackingGames.Foundations.Hastad.walsh_support line 453
63. theorem OAI.BinPackingGames.Foundations.Hastad.sign_power_parity line 461
64. theorem OAI.BinPackingGames.Foundations.Hastad.walsh_pullback line 471
65. theorem OAI.BinPackingGames.Foundations.Hastad.projectedCoefficient_eq line 481
66. theorem OAI.BinPackingGames.Foundations.Hastad.projection_has_preimage line 486
67. theorem OAI.BinPackingGames.Foundations.Hastad.scaled_geometric_power_le_one line 498
68. theorem OAI.BinPackingGames.Foundations.Hastad.noise_decay_bound line 512
69. def OAI.BinPackingGames.Foundations.Hastad.zeroMask line 525
70. theorem OAI.BinPackingGames.Foundations.Hastad.support_eq_empty_iff line 528
71. theorem OAI.BinPackingGames.Foundations.Hastad.parityProjection_zero line 540
72. def OAI.BinPackingGames.Foundations.Hastad.agreementProbability line 545
73. theorem OAI.BinPackingGames.Foundations.Hastad.agreementProbability_nonneg line 550
74. theorem OAI.BinPackingGames.Foundations.Hastad.agreementProbability_projection line 558
75. def OAI.BinPackingGames.Foundations.Hastad.decoderSuccess line 584
76. def OAI.BinPackingGames.Foundations.Hastad.decodingEnergy line 588
77. theorem OAI.BinPackingGames.Foundations.Hastad.decodingEnergy_le_success line 591
78. theorem OAI.BinPackingGames.Foundations.Hastad.bias_sq_le_weighted_energy line 625
79. theorem OAI.BinPackingGames.Foundations.Hastad.decoder_four_epsilon_bias_sq line 642
80. theorem OAI.BinPackingGames.Foundations.Hastad.folded_decoder_bound line 668
81. def OAI.BinPackingGames.Foundations.Hastad.validAgreementProbability line 676
82. theorem OAI.BinPackingGames.Foundations.Hastad.validAgreementProbability_eq line 683
83. def OAI.BinPackingGames.Foundations.Hastad.validDecoderSuccess line 696
84. theorem OAI.BinPackingGames.Foundations.Hastad.conditioned_validDecoderSuccess line 702
85. theorem OAI.BinPackingGames.Foundations.Hastad.conditioned_folded_decoder_bound line 720
86. def OAI.BinPackingGames.Foundations.Hastad.SourceContexts.clauseAnswerEquiv line 738
87. def OAI.BinPackingGames.Foundations.Hastad.SourceContexts.clauseAnswerFinEquiv line 744
88. instance OAI.BinPackingGames.Foundations.Hastad.SourceContexts.clauseAnswerFintype line 750
89. instance OAI.BinPackingGames.Foundations.Hastad.SourceContexts.clauseAnswerInhabited line 753
90. instance OAI.BinPackingGames.Foundations.Hastad.SourceContexts.slotFintype line 755
91. instance OAI.BinPackingGames.Foundations.Hastad.SourceContexts.slotInhabited line 759
92. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.card_clauseAnswer line 761
93. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.card_slot line 765
94. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceContexts.I line 767
95. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceContexts.J line 768
96. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceContexts.ClauseContext line 769
97. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceContexts.VariableContext line 770
98. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceContexts.SlotContext line 771
99. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.card_I line 773
100. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.card_J line 774
101. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.card_ClauseContext line 775
102. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.card_VariableContext line 777
103. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.card_SlotContext line 779
104. def OAI.BinPackingGames.Foundations.Hastad.SourceContexts.localConsistent line 782
105. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.localConsistent_eq_true_iff line 786
106. def OAI.BinPackingGames.Foundations.Hastad.SourceContexts.validJ line 793
107. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.validJ_eq_true_iff line 798
108. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.validJ_satisfies line 806
109. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.validJ_consistent line 811
110. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.validJ_localConsistent line 818
111. def OAI.BinPackingGames.Foundations.Hastad.SourceContexts.canonicalSlot line 825
112. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.canonicalSlot_name line 829
113. def OAI.BinPackingGames.Foundations.Hastad.SourceContexts.pi line 841
114. def OAI.BinPackingGames.Foundations.Hastad.SourceContexts.sampledVariables line 845
115. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.sampledVariables_supported line 849
116. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.sampled_eq_pi line 854
117. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.sampled_answers_eq_of_visible_eq line 862
118. def OAI.BinPackingGames.Foundations.Hastad.SourceContexts.honestJ line 870
119. def OAI.BinPackingGames.Foundations.Hastad.SourceContexts.honestI line 874
120. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.honestJ_valid line 878
121. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.pi_honest line 890
122. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.pi_honest_sampled line 898
123. def OAI.BinPackingGames.Foundations.Hastad.SourceContexts.baseAccepts line 904
124. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.baseAccepts_eq_true_iff line 910
125. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.projection_implies_coordinate_accepts line 918
126. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.baseAccepts_implies_sampled line 925
127. theorem OAI.BinPackingGames.Foundations.Hastad.SourceContexts.projection_implies_sampled_accepts line 935
128. def OAI.BinPackingGames.Foundations.Hastad.supportResponse line 957
129. theorem OAI.BinPackingGames.Foundations.Hastad.supportResponse_expectation line 970
130. def OAI.BinPackingGames.Foundations.Hastad.fourierResponse line 981
131. theorem OAI.BinPackingGames.Foundations.Hastad.fourierResponse_expectation line 991
132. theorem OAI.BinPackingGames.Foundations.Hastad.response_expectation_nonnegative line 1006
133. def OAI.BinPackingGames.Foundations.Hastad.responseAgreement line 1011
134. def OAI.BinPackingGames.Foundations.Hastad.validResponseAgreement line 1016
135. theorem OAI.BinPackingGames.Foundations.Hastad.supportResponse_validAgreement line 1023
136. theorem OAI.BinPackingGames.Foundations.Hastad.validAgreement_le_supportResponses line 1037
137. theorem OAI.BinPackingGames.Foundations.Hastad.validDecoderSuccess_le_response line 1063
138. theorem OAI.BinPackingGames.Foundations.Hastad.conditioned_folded_response_bound line 1080
139. theorem OAI.BinPackingGames.Foundations.Hastad.distribution_sq_expectation_le line 1097
140. def OAI.BinPackingGames.Foundations.Hastad.projectionGame line 1127
141. def OAI.BinPackingGames.Foundations.Hastad.questionBias line 1132
142. def OAI.BinPackingGames.Foundations.Hastad.questionAcceptance line 1136
143. theorem OAI.BinPackingGames.Foundations.Hastad.questionAcceptance_eq line 1141
144. inductive OAI.BinPackingGames.Foundations.Hastad.ConditionedOracle line 1152
145. def OAI.BinPackingGames.Foundations.Hastad.ConditionedOracle.answer line 1156
146. def OAI.BinPackingGames.Foundations.Hastad.ConditionedOracle.fallback line 1160
147. theorem OAI.BinPackingGames.Foundations.Hastad.testBias_constant_right line 1166
148. theorem OAI.BinPackingGames.Foundations.Hastad.empty_conditioned_bias line 1173
149. theorem OAI.BinPackingGames.Foundations.Hastad.conditionedOracle_response_bound line 1183
150. theorem OAI.BinPackingGames.Foundations.Hastad.folded_game_decoder_bound line 1203
151. theorem OAI.BinPackingGames.Foundations.Hastad.conditionedOracle_game_decoder_bound line 1241
152. theorem OAI.BinPackingGames.Foundations.Hastad.conditionedOracle_acceptance_bound line 1277