OAI/Computability/MinUncut/PCP/PreprocessingTableSpectral.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTableSpectral.portGraph_ext line 11
  2. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTableSpectral.materialize_portGraph line 19
  3. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTableSpectral.overlay_portGraph line 29
  4. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTableSpectral.overlay_rotation_eq line 39
  5. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTableSpectral.lazy_portGraph line 48
  6. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTableSpectral.lazy_rotation_eq line 56
  7. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTableSpectral.overlay_certificate_seven_eighths line 64
  8. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingTableSpectral.lazy_certificate_31_32 line 80
  9. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingGuarantees.overlay_rejectionCount line 102
  10. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingGuarantees.lazy_rejectionCount line 116
  11. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingGuarantees.overlayFamily_certificate line 130
  12. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingGuarantees.overlay_certificate line 138
  13. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingGuarantees.spectral_certificate line 147
  14. def OAI.MinUncutGames.Foundations.PCP.PreprocessingGuarantees.restrictedLabel line 155
  15. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingGuarantees.rejectionCount_eq_regularized line 160
  16. def OAI.MinUncutGames.Foundations.PCP.PreprocessingGuarantees.roundLabels line 168
  17. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingGuarantees.soundness line 172
  18. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingGuarantees.completeness line 180
  19. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingGuarantees.gap_transfer_real line 193
  20. abbrev OAI.MinUncutGames.Foundations.PCP.PoweringLabels.PortWords line 234
  21. instance OAI.MinUncutGames.Foundations.PCP.PoweringLabels.finitePortWords line 236
  22. def OAI.MinUncutGames.Foundations.PCP.PoweringLabels.Ball line 240
  23. def OAI.MinUncutGames.Foundations.PCP.PoweringLabels.wordToBall line 243
  24. theorem OAI.MinUncutGames.Foundations.PCP.PoweringLabels.wordToBall_surjective line 246
  25. instance OAI.MinUncutGames.Foundations.PCP.PoweringLabels.finiteBall line 253
  26. theorem OAI.MinUncutGames.Foundations.PCP.PoweringLabels.card_portWords line 257
  27. theorem OAI.MinUncutGames.Foundations.PCP.PoweringLabels.card_ball_le line 261
  28. structure OAI.MinUncutGames.Foundations.PCP.PoweringLabels.AddressSelector line 268
  29. def OAI.MinUncutGames.Foundations.PCP.PoweringLabels.classicalSelector line 272
  30. def OAI.MinUncutGames.Foundations.PCP.PoweringLabels.scanWitness line 277
  31. def OAI.MinUncutGames.Foundations.PCP.PoweringLabels.listSelector line 288
  32. abbrev OAI.MinUncutGames.Foundations.PCP.PoweringLabels.PaddedLabel line 299
  33. def OAI.MinUncutGames.Foundations.PCP.PoweringLabels.encode line 301
  34. def OAI.MinUncutGames.Foundations.PCP.PoweringLabels.decode line 304
  35. theorem OAI.MinUncutGames.Foundations.PCP.PoweringLabels.decode_encode line 307
  36. theorem OAI.MinUncutGames.Foundations.PCP.PoweringLabels.decode_surjective line 314
  37. theorem OAI.MinUncutGames.Foundations.PCP.PoweringLabels.encode_injective line 318
  38. theorem OAI.MinUncutGames.Foundations.PCP.PoweringLabels.decoded_word_collision line 325
  39. theorem OAI.MinUncutGames.Foundations.PCP.PoweringLabels.card_paddedLabel line 331
  40. def OAI.MinUncutGames.Foundations.PCP.PoweringAddresses.allWords line 347
  41. theorem OAI.MinUncutGames.Foundations.PCP.PoweringAddresses.mem_allWords line 352
  42. def OAI.MinUncutGames.Foundations.PCP.PoweringAddresses.allAddresses line 368
  43. theorem OAI.MinUncutGames.Foundations.PCP.PoweringAddresses.mem_allAddresses line 372
  44. theorem OAI.MinUncutGames.Foundations.PCP.PoweringAddresses.length_allWords line 380
  45. theorem OAI.MinUncutGames.Foundations.PCP.PoweringAddresses.length_allAddresses line 390
  46. def OAI.MinUncutGames.Foundations.PCP.PoweringAddresses.finitePortSelector line 396
  47. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.addressCount line 409
  48. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.reverseWordEquiv line 411
  49. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.wordEquiv line 417
  50. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.wordEquiv_val line 420
  51. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.addressEquiv line 423
  52. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.addressEquiv_val line 427
  53. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.paddedLabelEquiv line 435
  54. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.paddedLabelEquiv_val line 440
  55. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.orientationEquiv line 445
  56. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.orientationEquiv_false line 447
  57. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.orientationEquiv_true line 448
  58. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.dartBlockEquiv line 450
  59. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.dartBlockEquiv_val line 455
  60. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.dartVertexEquiv line 461
  61. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.dartEquiv line 469
  62. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.dartEquiv_val line 478
  63. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.dartEquiv_true_eq_false_add_one line 487
  64. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.encodeWord line 494
  65. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.decodeWord line 495
  66. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.decodeWord_encodeWord line 497
  67. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.encodeWord_decodeWord line 500
  68. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.encodeAddress line 503
  69. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.decodeAddress line 506
  70. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.decodeAddress_encodeAddress line 509
  71. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.encodeAddress_decodeAddress line 512
  72. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.encodeLabel line 515
  73. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.decodeLabel line 518
  74. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.decodeLabel_encodeLabel line 522
  75. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.encodeLabel_decodeLabel line 525
  76. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.decodeLabel_apply line 528
  77. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.encodeDart line 532
  78. def OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.decodeDart line 536
  79. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.decodeDart_encodeDart line 540
  80. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.encodeDart_decodeDart line 545
  81. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.card_words line 550
  82. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.card_addresses line 553
  83. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.card_labels line 557
  84. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.card_darts line 561
  85. theorem OAI.MinUncutGames.Foundations.PCP.PoweringEnumeration.length_allAddresses line 566
  86. def OAI.MinUncutGames.Foundations.PCP.PoweringDecoding.mass line 580
  87. theorem OAI.MinUncutGames.Foundations.PCP.PoweringDecoding.mass_sum line 585
  88. theorem OAI.MinUncutGames.Foundations.PCP.PoweringDecoding.exists_mode line 600
  89. def OAI.MinUncutGames.Foundations.PCP.PoweringDecoding.mode line 606
  90. theorem OAI.MinUncutGames.Foundations.PCP.PoweringDecoding.mode_max line 609
  91. theorem OAI.MinUncutGames.Foundations.PCP.PoweringDecoding.mode_mass_lower line 613
  92. theorem OAI.MinUncutGames.Foundations.PCP.PoweringDecoding.exists_letter_mass_lower line 624
  93. def OAI.MinUncutGames.Foundations.PCP.PoweringMoment.bit line 638
  94. def OAI.MinUncutGames.Foundations.PCP.PoweringMoment.hits line 642
  95. def OAI.MinUncutGames.Foundations.PCP.PoweringMoment.mean line 645
  96. theorem OAI.MinUncutGames.Foundations.PCP.PoweringMoment.bit_nonneg line 647
  97. theorem OAI.MinUncutGames.Foundations.PCP.PoweringMoment.bit_sq line 651
  98. theorem OAI.MinUncutGames.Foundations.PCP.PoweringMoment.bit_mul line 655
  99. theorem OAI.MinUncutGames.Foundations.PCP.PoweringMoment.bit_mono line 659
  100. theorem OAI.MinUncutGames.Foundations.PCP.PoweringMoment.hits_nonneg line 667
  101. theorem OAI.MinUncutGames.Foundations.PCP.PoweringMoment.mean_nonneg line 670
  102. theorem OAI.MinUncutGames.Foundations.PCP.PoweringMoment.mean_hits line 673
  103. theorem OAI.MinUncutGames.Foundations.PCP.PoweringMoment.second_moment_eq line 677
  104. theorem OAI.MinUncutGames.Foundations.PCP.PoweringMoment.mean_witness_sq_le line 685
  105. theorem OAI.MinUncutGames.Foundations.PCP.PoweringMoment.rejection_lower_bound line 717