OAI/Computability/DirectedFeedback/Encoding/PoweringAddresses.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.PCP.PoweringAddresses.allWords line 13
2. theorem OAI.DFVSGames.Foundations.PCP.PoweringAddresses.mem_allWords line 18
3. def OAI.DFVSGames.Foundations.PCP.PoweringAddresses.allAddresses line 34
4. theorem OAI.DFVSGames.Foundations.PCP.PoweringAddresses.mem_allAddresses line 38
5. theorem OAI.DFVSGames.Foundations.PCP.PoweringAddresses.length_allWords line 46
6. theorem OAI.DFVSGames.Foundations.PCP.PoweringAddresses.length_allAddresses line 56
7. def OAI.DFVSGames.Foundations.PCP.PoweringAddresses.finitePortSelector line 62
8. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.addressCount line 73
9. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.reverseWordEquiv line 75
10. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.wordEquiv line 81
11. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.wordEquiv_val line 84
12. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.addressEquiv line 87
13. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.addressEquiv_val line 91
14. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.paddedLabelEquiv line 99
15. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.paddedLabelEquiv_val line 104
16. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.orientationEquiv line 109
17. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.orientationEquiv_false line 111
18. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.orientationEquiv_true line 112
19. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.dartBlockEquiv line 114
20. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.dartBlockEquiv_val line 119
21. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.dartVertexEquiv line 125
22. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.dartEquiv line 133
23. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.dartEquiv_val line 142
24. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.dartEquiv_true_eq_false_add_one line 151
25. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.encodeWord line 158
26. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.decodeWord line 159
27. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.decodeWord_encodeWord line 161
28. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.encodeWord_decodeWord line 164
29. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.encodeAddress line 167
30. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.decodeAddress line 170
31. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.decodeAddress_encodeAddress line 173
32. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.encodeAddress_decodeAddress line 176
33. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.encodeLabel line 179
34. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.decodeLabel line 182
35. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.decodeLabel_encodeLabel line 186
36. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.encodeLabel_decodeLabel line 189
37. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.decodeLabel_apply line 192
38. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.encodeDart line 196
39. def OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.decodeDart line 200
40. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.decodeDart_encodeDart line 204
41. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.encodeDart_decodeDart line 209
42. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.card_words line 214
43. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.card_addresses line 217
44. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.card_labels line 221
45. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.card_darts line 225
46. theorem OAI.DFVSGames.Foundations.PCP.PoweringEnumeration.length_allAddresses line 230
47. def OAI.DFVSGames.Foundations.PCP.PoweringDecoding.mass line 242
48. theorem OAI.DFVSGames.Foundations.PCP.PoweringDecoding.mass_sum line 247
49. theorem OAI.DFVSGames.Foundations.PCP.PoweringDecoding.exists_mode line 262
50. def OAI.DFVSGames.Foundations.PCP.PoweringDecoding.mode line 268
51. theorem OAI.DFVSGames.Foundations.PCP.PoweringDecoding.mode_max line 271
52. theorem OAI.DFVSGames.Foundations.PCP.PoweringDecoding.mode_mass_lower line 275
53. theorem OAI.DFVSGames.Foundations.PCP.PoweringDecoding.exists_letter_mass_lower line 286
54. def OAI.DFVSGames.Foundations.PCP.PoweringMoment.bit line 298
55. def OAI.DFVSGames.Foundations.PCP.PoweringMoment.hits line 302
56. def OAI.DFVSGames.Foundations.PCP.PoweringMoment.mean line 305
57. theorem OAI.DFVSGames.Foundations.PCP.PoweringMoment.bit_nonneg line 307
58. theorem OAI.DFVSGames.Foundations.PCP.PoweringMoment.bit_sq line 311
59. theorem OAI.DFVSGames.Foundations.PCP.PoweringMoment.bit_mul line 315
60. theorem OAI.DFVSGames.Foundations.PCP.PoweringMoment.bit_mono line 319
61. theorem OAI.DFVSGames.Foundations.PCP.PoweringMoment.hits_nonneg line 327
62. theorem OAI.DFVSGames.Foundations.PCP.PoweringMoment.mean_nonneg line 330
63. theorem OAI.DFVSGames.Foundations.PCP.PoweringMoment.mean_hits line 333
64. theorem OAI.DFVSGames.Foundations.PCP.PoweringMoment.second_moment_eq line 337
65. theorem OAI.DFVSGames.Foundations.PCP.PoweringMoment.mean_witness_sq_le line 345
66. theorem OAI.DFVSGames.Foundations.PCP.PoweringMoment.rejection_lower_bound line 377
67. def OAI.DFVSGames.Foundations.PCP.PoweringReturn.portConsEquiv line 404
68. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.mean_word_cons_head line 417
69. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.mean_word_cons_tail line 425
70. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.iterateOperator_succ_right line 433
71. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.mean_wordEnd line 440
72. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.mean_pivot_endpoints line 461
73. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.mean_edge_endpoints line 503
74. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.bit_bool line 527
75. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.mean_edge_bit line 530
76. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.mean_marked_bit line 534
77. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.edgeAt_zero line 544
78. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.word_first_hit_mean line 548
79. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.word_hit_mean line 559
80. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.word_pair_hit_mean line 586
81. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.hit_mean line 644
82. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.pair_hit_mean line 660
83. theorem OAI.DFVSGames.Foundations.PCP.PoweringReturn.pair_event_mean line 681
84. def OAI.DFVSGames.Foundations.PCP.PoweringOpinions.opinionAt line 700
85. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinions.opinionAt_eq_decode line 707
86. def OAI.DFVSGames.Foundations.PCP.PoweringOpinions.honestLabels line 715
87. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinions.opinionAt_honest line 718
88. def OAI.DFVSGames.Foundations.PCP.PoweringOpinions.sampleOpinion line 728
89. def OAI.DFVSGames.Foundations.PCP.PoweringOpinions.decoded line 733
90. def OAI.DFVSGames.Foundations.PCP.PoweringOpinions.matchFn line 738
91. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinions.matchFn_mem_Icc line 744
92. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinions.decoded_modal_baseline line 754
93. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinions.decoded_modal_near line 764