OAI/Computability/DirectedFeedback/Games/Preprocessing.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Foundations.PCP.LazySpectral.half_sum_sq_le line 15
  2. theorem OAI.DFVSGames.Foundations.PCP.LazySpectral.lazy_energy_le_average line 18
  3. theorem OAI.DFVSGames.Foundations.PCP.LazySpectral.lazy_energy_bound line 40
  4. theorem OAI.DFVSGames.Foundations.PCP.LazySpectral.lazy_certificate_31_32 line 53
  5. abbrev OAI.DFVSGames.Foundations.PCP.Preprocessing.Vertex line 76
  6. abbrev OAI.DFVSGames.Foundations.PCP.Preprocessing.OverlayPort line 77
  7. abbrev OAI.DFVSGames.Foundations.PCP.Preprocessing.Port line 78
  8. def OAI.DFVSGames.Foundations.PCP.Preprocessing.degree line 80
  9. def OAI.DFVSGames.Foundations.PCP.Preprocessing.sizeFactor line 81
  10. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.card_lazy_sum_inline_Preprocessing line 83
  11. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.doubled_add_inline_Preprocessing line 88
  12. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.degree_eq_card line 90
  13. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.degree_positive line 99
  14. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.sizeFactor_positive line 103
  15. def OAI.DFVSGames.Foundations.PCP.Preprocessing.paddedGraph line 108
  16. def OAI.DFVSGames.Foundations.PCP.Preprocessing.overlayExpander line 112
  17. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.overlayExpander_certificate line 119
  18. def OAI.DFVSGames.Foundations.PCP.Preprocessing.overlayGraph line 123
  19. def OAI.DFVSGames.Foundations.PCP.Preprocessing.graph line 127
  20. def OAI.DFVSGames.Foundations.PCP.Preprocessing.portGraph line 131
  21. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.graph_tail line 135
  22. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.graph_reverse line 138
  23. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.accepts_reverse line 142
  24. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.portGraph_eq_lazyGraph line 147
  25. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.overlayGraph_certificate line 151
  26. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.spectral_certificate line 161
  27. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.vertex_count_le line 168
  28. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.dart_count line 178
  29. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.dart_count_le line 184
  30. def OAI.DFVSGames.Foundations.PCP.Preprocessing.liftLabel line 192
  31. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.lift_rejectionCount line 198
  32. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.completeness line 210
  33. def OAI.DFVSGames.Foundations.PCP.Preprocessing.roundLabels line 217
  34. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.soundness line 222
  35. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.satisfiable_iff line 235
  36. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.gap_transfer line 247
  37. theorem OAI.DFVSGames.Foundations.PCP.Preprocessing.gap_transfer_real line 263
  38. abbrev OAI.DFVSGames.Foundations.PCP.PreprocessingTables.BaseTable line 286
  39. def OAI.DFVSGames.Foundations.PCP.PreprocessingTables.degree line 288
  40. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTables.degree_eq line 290
  41. def OAI.DFVSGames.Foundations.PCP.PreprocessingTables.regularVertices line 295
  42. def OAI.DFVSGames.Foundations.PCP.PreprocessingTables.vertices line 296
  43. def OAI.DFVSGames.Foundations.PCP.PreprocessingTables.padded line 298
  44. def OAI.DFVSGames.Foundations.PCP.PreprocessingTables.overlayFamily line 303
  45. def OAI.DFVSGames.Foundations.PCP.PreprocessingTables.preprocess line 308
  46. def OAI.DFVSGames.Foundations.PCP.PreprocessingTables.output line 313
  47. def OAI.DFVSGames.Foundations.PCP.PreprocessingTables.graphTable line 316
  48. def OAI.DFVSGames.Foundations.PCP.PreprocessingTables.outputBits line 319
  49. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTables.regularVertices_ge_darts line 322
  50. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTables.regularVertices_le line 326
  51. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTables.vertices_positive line 329
  52. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTables.vertices_le_of_positive line 332
  53. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTables.vertices_eq_one_of_no_darts line 342
  54. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTables.vertices_le line 347
  55. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTables.darts_eq line 357
  56. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTables.darts_le line 360
  57. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTables.vertices_le_inputBits line 368
  58. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTables.darts_le_inputBits line 373
  59. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularSoundness.internalDegree_ge_eight line 385
  60. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularSoundness.baseDegree_ne_zero line 389
  61. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularSoundness.resizeTable_certificate line 395
  62. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularSoundness.familyCloudTable_certificate_of_pos line 402
  63. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularSoundness.cloudGraphs_certificate_of_pos line 413
  64. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularSoundness.cloud_expansion line 422
  65. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularSoundness.roundLabels line 444
  66. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularSoundness.soundness line 451
  67. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularSoundness.exists_rounding line 462
  68. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularSoundness.lift_rejectionCount line 471
  69. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularSoundness.completeness line 477
  70. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularSoundness.soundness_of_uniform_lower_bound line 499
  71. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularSoundness.soundness_of_uniform_real_lower_bound line 508
  72. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTableSpectral.portGraph_ext_inline_PreprocessingTableSpectral line 523
  73. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTableSpectral.materialize_portGraph line 531
  74. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTableSpectral.overlay_portGraph line 541
  75. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTableSpectral.overlay_rotation_eq line 551
  76. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTableSpectral.lazy_portGraph line 560
  77. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTableSpectral.lazy_rotation_eq line 568
  78. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTableSpectral.overlay_certificate_seven_eighths line 576
  79. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingTableSpectral.lazy_certificate_31_32 line 592
  80. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingGuarantees.overlay_rejectionCount line 612
  81. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingGuarantees.lazy_rejectionCount line 625
  82. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingGuarantees.overlayFamily_certificate line 638
  83. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingGuarantees.overlay_certificate line 646
  84. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingGuarantees.spectral_certificate line 655
  85. def OAI.DFVSGames.Foundations.PCP.PreprocessingGuarantees.restrictedLabel line 663
  86. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingGuarantees.rejectionCount_eq_regularized line 668
  87. def OAI.DFVSGames.Foundations.PCP.PreprocessingGuarantees.roundLabels line 676
  88. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingGuarantees.soundness line 680
  89. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingGuarantees.completeness line 688
  90. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingGuarantees.gap_transfer_real line 701
  91. abbrev OAI.DFVSGames.Foundations.PCP.PoweringLabels.PortWords line 740
  92. instance OAI.DFVSGames.Foundations.PCP.PoweringLabels.finitePortWords line 742
  93. def OAI.DFVSGames.Foundations.PCP.PoweringLabels.Ball line 746
  94. def OAI.DFVSGames.Foundations.PCP.PoweringLabels.wordToBall line 749
  95. theorem OAI.DFVSGames.Foundations.PCP.PoweringLabels.wordToBall_surjective line 752
  96. instance OAI.DFVSGames.Foundations.PCP.PoweringLabels.finiteBall line 759
  97. theorem OAI.DFVSGames.Foundations.PCP.PoweringLabels.card_portWords line 763
  98. theorem OAI.DFVSGames.Foundations.PCP.PoweringLabels.card_ball_le line 767
  99. structure OAI.DFVSGames.Foundations.PCP.PoweringLabels.AddressSelector line 774
  100. def OAI.DFVSGames.Foundations.PCP.PoweringLabels.classicalSelector line 778
  101. def OAI.DFVSGames.Foundations.PCP.PoweringLabels.scanWitness line 783
  102. def OAI.DFVSGames.Foundations.PCP.PoweringLabels.listSelector line 794
  103. abbrev OAI.DFVSGames.Foundations.PCP.PoweringLabels.PaddedLabel line 805
  104. def OAI.DFVSGames.Foundations.PCP.PoweringLabels.encode line 807
  105. def OAI.DFVSGames.Foundations.PCP.PoweringLabels.decode line 810
  106. theorem OAI.DFVSGames.Foundations.PCP.PoweringLabels.decode_encode line 813
  107. theorem OAI.DFVSGames.Foundations.PCP.PoweringLabels.decode_surjective line 820
  108. theorem OAI.DFVSGames.Foundations.PCP.PoweringLabels.encode_injective line 824
  109. theorem OAI.DFVSGames.Foundations.PCP.PoweringLabels.decoded_word_collision line 831
  110. theorem OAI.DFVSGames.Foundations.PCP.PoweringLabels.card_paddedLabel line 837