OAI/Computability/DirectedFeedback/Encoding/PoweringTables.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.PCP.PoweringTables.labelCount line 11
  2. def OAI.DFVSGames.Foundations.PCP.PoweringTables.dartCount line 13
  3. def OAI.DFVSGames.Foundations.PCP.PoweringTables.mathematicalGraph line 15
  4. def OAI.DFVSGames.Foundations.PCP.PoweringTables.rowAccepts line 21
  5. theorem OAI.DFVSGames.Foundations.PCP.PoweringTables.rowAccepts_eq line 30
  6. def OAI.DFVSGames.Foundations.PCP.PoweringTables.table line 40
  7. theorem OAI.DFVSGames.Foundations.PCP.PoweringTables.table_vertices line 45
  8. theorem OAI.DFVSGames.Foundations.PCP.PoweringTables.table_darts line 48
  9. theorem OAI.DFVSGames.Foundations.PCP.PoweringTables.semantics_table line 51
  10. theorem OAI.DFVSGames.Foundations.PCP.PoweringTables.table_accepts line 57
  11. theorem OAI.DFVSGames.Foundations.PCP.PoweringTables.table_reverse line 65
  12. def OAI.DFVSGames.Foundations.PCP.PoweringTables.outputBits line 77
  13. def OAI.DFVSGames.Foundations.PCP.PoweringTables.transform line 80
  14. theorem OAI.DFVSGames.Foundations.PCP.PoweringCounting.constraint_rejection_mean_eq_count line 93
  15. theorem OAI.DFVSGames.Foundations.PCP.PoweringCounting.constraint_rejection_lower_iff line 108
  16. theorem OAI.DFVSGames.Foundations.PCP.PoweringCounting.edgeDensity_eq_bit_mean line 117
  17. theorem OAI.DFVSGames.Foundations.PCP.PoweringCounting.base_edgeDensity_eq_rejection_count line 131
  18. theorem OAI.DFVSGames.Foundations.PCP.PoweringCounting.base_count_lower_to_density line 149
  19. theorem OAI.DFVSGames.Foundations.PCP.PoweringCounting.powered_rejection_mean_eq_count line 159
  20. theorem OAI.DFVSGames.Foundations.PCP.PoweringCounting.path_rejection_mean_eq_count line 169
  21. theorem OAI.DFVSGames.Foundations.PCP.PoweringCounting.powered_density_lower_to_count line 180
  22. theorem OAI.DFVSGames.Foundations.PCP.PoweringCounting.natCard_dart line 192
  23. theorem OAI.DFVSGames.Foundations.PCP.PoweringCounting.fintypeCard_dart line 196
  24. theorem OAI.DFVSGames.Foundations.PCP.PoweringCounting.natCard_poweredAlphabet line 201
  25. theorem OAI.DFVSGames.Foundations.PCP.PoweringCounting.natCard_finitePortAlphabet line 206
  26. abbrev OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.RawLabeling line 219
  27. abbrev OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.EncodedLabeling line 222
  28. def OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.encodeLabeling line 225
  29. def OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.decodeLabeling line 229
  30. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.decodeLabeling_encodeLabeling line 233
  31. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.encodeLabeling_decodeLabeling line 239
  32. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_encoded line 246
  33. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_decoded line 257
  34. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.edgeSatisfied_eq_path line 266
  35. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.rejectionCount_encoded line 281
  36. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.rejectionCount_decoded line 291
  37. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.card_darts_eq_table line 298
  38. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.satisfiable_iff line 305
  39. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.preserves_satisfiability line 322
  40. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.path_rejection_mean_eq_table_fraction line 330
  41. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.uniform_count_gap_iff line 345
  42. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableSemantics.uniform_count_gap line 364
  43. structure OAI.DFVSGames.Foundations.PCP.QueryIncidence.Verifier line 380
  44. abbrev OAI.DFVSGames.Foundations.PCP.QueryIncidence.Label line 384
  45. abbrev OAI.DFVSGames.Foundations.PCP.QueryIncidence.Vertex line 385
  46. abbrev OAI.DFVSGames.Foundations.PCP.QueryIncidence.Dart line 386
  47. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.response line 390
  48. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.zeroSlot line 393
  49. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.decodeRight line 395
  50. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.encodeRight line 397
  51. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.decode_encodeRight line 399
  52. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.canonicalSlot line 402
  53. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.canonicalSlot_query line 405
  54. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.RepeatedConsistent line 409
  55. instance OAI.DFVSGames.Foundations.PCP.QueryIncidence.repeatedConsistentDecidable line 412
  56. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.LeftValid line 418
  57. instance OAI.DFVSGames.Foundations.PCP.QueryIncidence.leftValidDecidable line 421
  58. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.incidenceAccept line 427
  59. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.reverse line 432
  60. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.reverse_involutive line 434
  61. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.reverseEquiv line 438
  62. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.tail line 444
  63. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.predicate line 448
  64. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.graph line 453
  65. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.edgeSatisfied_eq_incidence line 463
  66. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.honestLabeling line 471
  67. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.honest_leftValid line 475
  68. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.honest_incidence line 482
  69. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.perfect_completeness line 493
  70. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.satisfiable_of_verifier_satisfiable line 501
  71. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.decodedAssignment line 509
  72. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.incidenceAccept_true line 512
  73. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.all_incidences_imply_event line 521
  74. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.rejected_event_forces_slot line 536
  75. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.rejectedEvents line 554
  76. def OAI.DFVSGames.Foundations.PCP.QueryIncidence.verifierRejectionCount line 557
  77. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.rejection_count_bound line 560
  78. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.card_label line 589
  79. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.card_vertex line 592
  80. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.card_dart line 596
  81. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.gap_transfer line 600
  82. theorem OAI.DFVSGames.Foundations.PCP.QueryIncidence.six_query_alphabet line 615
  83. def OAI.DFVSGames.Foundations.PCP.CodeComposition.disagreement line 628
  84. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.disagreement_self line 630
  85. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.disagreement_nonnegative line 633
  86. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.disagreement_le_one line 636
  87. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.disagreement_comm line 639
  88. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.disagreement_triangle line 642
  89. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.disagreement_eq_sign line 646
  90. def OAI.DFVSGames.Foundations.PCP.CodeComposition.relativeDistance line 650
  91. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.relativeDistance_self line 653
  92. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.relativeDistance_nonnegative line 657
  93. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.relativeDistance_comm line 661
  94. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.relativeDistance_triangle line 665
  95. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.relativeDistance_eq_sign line 671
  96. def OAI.DFVSGames.Foundations.PCP.CodeComposition.codeword line 678
  97. def OAI.DFVSGames.Foundations.PCP.CodeComposition.singletonMask_inline_CodeComposition line 680
  98. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.walsh_singletonMask_inline_CodeComposition line 683
  99. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.singletonMask_ne_inline_CodeComposition line 693
  100. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.codeword_distance line 699
  101. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.exists_nearest line 710
  102. def OAI.DFVSGames.Foundations.PCP.CodeComposition.nearest line 718
  103. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.nearest_minimal line 721
  104. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.distance_from_other_codeword line 726
  105. def OAI.DFVSGames.Foundations.PCP.CodeComposition.pairWord line 734
  106. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.pairWord_distance line 737
  107. theorem OAI.DFVSGames.Foundations.PCP.CodeComposition.rejected_pair_far line 746