OAI/Computability/DirectedFeedback/Games/StageData.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Gadget.StageData.toData line 16
2. theorem OAI.DFVSGames.Gadget.StageData.count_probability_eq_expect line 29
3. theorem OAI.DFVSGames.Gadget.StageData.count_probability_eq_harmonic line 36
4. theorem OAI.DFVSGames.Gadget.StageData.stabilityError_toData line 44
5. theorem OAI.DFVSGames.Gadget.StageData.stabilityError_toData_count line 58
6. theorem OAI.DFVSGames.Gadget.StageData.error_eq_count_probability line 75
7. theorem OAI.DFVSGames.Gadget.StageData.kernelError_toData_count line 88
8. theorem OAI.DFVSGames.Gadget.StageData.kernelError_eq_one_sub_detection line 100
9. theorem OAI.DFVSGames.Gadget.StageData.kernelError_le_of_detection line 121
10. def OAI.DFVSGames.Gadget.EnlargementEndpoint.data line 149
11. theorem OAI.DFVSGames.Gadget.EnlargementEndpoint.data_satisfies line 157
12. theorem OAI.DFVSGames.Gadget.EnlargementEndpoint.exists_data line 186
13. theorem OAI.DFVSGames.Gadget.exists_actual_gadget line 210
14. theorem OAI.DFVSGames.Gadget.exists_split_gadget line 259
15. theorem OAI.DFVSGames.Decoder.MatrixGap.parameters_of_inverse line 285
16. def OAI.DFVSGames.Appendix.Restriction.isum line 331
17. theorem OAI.DFVSGames.Appendix.Restriction.isum_congr line 335
18. theorem OAI.DFVSGames.Appendix.Restriction.isum_zero line 341
19. theorem OAI.DFVSGames.Appendix.Restriction.isum_add line 346
20. theorem OAI.DFVSGames.Appendix.Restriction.isum_mul_left line 352
21. theorem OAI.DFVSGames.Appendix.Restriction.isum_mul_right line 358
22. theorem OAI.DFVSGames.Appendix.Restriction.isum_const line 364
23. theorem OAI.DFVSGames.Appendix.Restriction.isum_swap line 373
24. theorem OAI.DFVSGames.Appendix.Restriction.isum_map line 379
25. theorem OAI.DFVSGames.Appendix.Restriction.isum_perm line 385
26. def OAI.DFVSGames.Appendix.Restriction.binarySign line 393
27. theorem OAI.DFVSGames.Appendix.Restriction.binarySign_xor line 395
28. theorem OAI.DFVSGames.Appendix.Restriction.binary_character_restriction line 399
29. theorem OAI.DFVSGames.Appendix.Restriction.coefficient_merging line 409
30. theorem OAI.DFVSGames.Appendix.Restriction.restriction_average line 448
31. theorem OAI.DFVSGames.Appendix.Restriction.bool_translation_perm line 463
32. theorem OAI.DFVSGames.Appendix.Restriction.bool_restriction_average line 469
33. theorem OAI.DFVSGames.Appendix.Restriction.bool_character_compatibility line 474
34. theorem OAI.DFVSGames.Appendix.Restriction.bool_character_orthogonality line 478
35. theorem OAI.DFVSGames.Appendix.Restriction.bool_coefficient_merging line 483
36. theorem OAI.DFVSGames.Appendix.Restriction.real_translation_average line 503
37. def OAI.DFVSGames.Appendix.Restriction.compressFrequency line 518
38. theorem OAI.DFVSGames.Appendix.Restriction.linear_trace_restriction line 524
39. theorem OAI.DFVSGames.Appendix.Restriction.linear_character_restriction line 535
40. theorem OAI.DFVSGames.Appendix.Restriction.real_character_restriction line 544
41. theorem OAI.DFVSGames.Appendix.Restriction.linear_restriction_average line 557
42. theorem OAI.DFVSGames.Appendix.Restriction.linear_restriction_moment_average line 564
43. theorem OAI.DFVSGames.Appendix.Restriction.linear_coefficient_merging line 573
44. def OAI.DFVSGames.Appendix.Level.rankFilter line 606
45. theorem OAI.DFVSGames.Appendix.Level.filter_polynomial_algebra line 610
46. theorem OAI.DFVSGames.Appendix.Level.rankFilter_selected line 614
47. theorem OAI.DFVSGames.Appendix.Level.rankFilter_zero_at_d line 617
48. theorem OAI.DFVSGames.Appendix.Level.rankFilter_zero_at_pred line 621
49. theorem OAI.DFVSGames.Appendix.Level.only_two_source_ranks line 625
50. theorem OAI.DFVSGames.Appendix.Level.rank_filter_character line 630
51. def OAI.DFVSGames.Appendix.Level.mergedCoefficient line 648
52. theorem OAI.DFVSGames.Appendix.Level.rank_filter_commutes_with_merge line 652
53. theorem OAI.DFVSGames.Appendix.Level.higher_ranks_cannot_contaminate line 671
54. theorem OAI.DFVSGames.Appendix.Level.iterated_globality_exponent line 675
55. theorem OAI.DFVSGames.Appendix.Level.successor_le_two_pow line 685
56. theorem OAI.DFVSGames.Appendix.Level.selector_multiplicity_bound line 692
57. theorem OAI.DFVSGames.Appendix.Level.final_exponent_slack line 705
58. def OAI.DFVSGames.Appendix.Level.LinearRank.compress line 718
59. theorem OAI.DFVSGames.Appendix.Level.LinearRank.finrank_comap_subtype_le line 721
60. theorem OAI.DFVSGames.Appendix.Level.LinearRank.quotient_rank_bounds line 727
61. theorem OAI.DFVSGames.Appendix.Level.LinearRank.quotient_rank_selected line 738
62. theorem OAI.DFVSGames.Appendix.Level.LinearRank.domain_rank_bounds line 749
63. theorem OAI.DFVSGames.Appendix.Level.LinearRank.domain_rank_selected line 764
64. theorem OAI.DFVSGames.Appendix.Level.LinearRank.hybrid_rank_loss line 776
65. theorem OAI.DFVSGames.Appendix.Level.LinearRank.finrank_comap_subtype_eq_iff line 787
66. theorem OAI.DFVSGames.Appendix.Level.LinearRank.quotient_rank_equality_iff line 800
67. theorem OAI.DFVSGames.Appendix.Level.LinearRank.domain_rank_equality_iff line 814
68. theorem OAI.DFVSGames.Appendix.Level.LinearRank.compression_rank_bounds line 827
69. theorem OAI.DFVSGames.Appendix.Level.LinearRank.hybrid_rank_loss_iff line 838
70. theorem OAI.DFVSGames.Appendix.Level.LinearRank.line_rank_filter line 860
71. theorem OAI.DFVSGames.Appendix.Level.LinearRank.hyperplane_rank_filter line 881