OAI/Computability/MinUncut/PCP/PoweringFinalConstants.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.PCP.PoweringFinalConstants.Alphabet line 10
  2. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFinalConstants.card_alphabet line 12
  3. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFinalConstants.card_alphabet_eq_final line 15
  4. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFinalConstants.center_eq line 18
  5. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFinalConstants.walkLength_eq line 24
  6. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFinalConstants.spectral_denominator_eq line 30
  7. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFinalConstants.gain_eq line 34
  8. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFinalConstants.gain_card_eq line 52
  9. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFinalConstants.scaled_bound_eq line 58
  10. theorem OAI.MinUncutGames.Foundations.PCP.PoweringFinalConstants.composed_scaled_gap line 68
  11. def OAI.MinUncutGames.Foundations.PCP.RoundGap.poweredLower line 90
  12. theorem OAI.MinUncutGames.Foundations.PCP.RoundGap.poweredLower_nonnegative line 94
  13. theorem OAI.MinUncutGames.Foundations.PCP.RoundGap.powered_count_gap line 102
  14. theorem OAI.MinUncutGames.Foundations.PCP.RoundGap.amplifies line 130
  15. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.card_padded_alphabet line 155
  16. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.card_powered_dart line 162
  17. opaque OAI.MinUncutGames.Foundations.PCP.RoundSize.lockedNat line 169
  18. def OAI.MinUncutGames.Foundations.PCP.RoundSize.poweredAlphabetSize line 171
  19. def OAI.MinUncutGames.Foundations.PCP.RoundSize.poweredDartFactor line 175
  20. def OAI.MinUncutGames.Foundations.PCP.RoundSize.sizeFactor line 178
  21. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.poweredAlphabetSize_eq line 182
  22. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.poweredDartFactor_eq line 186
  23. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.sizeFactor_eq line 190
  24. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.coefficient_positive line 194
  25. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.poweredAlphabet_card line 199
  26. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.sizeFactor_positive line 208
  27. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.factor_total line 214
  28. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.nat_card_output_vertex line 217
  29. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.nat_card_output_dart line 225
  30. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.nat_card_output_total_le line 232
  31. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.poweredDart_card line 244
  32. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.output_vertex_card line 255
  33. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.output_dart_card line 270
  34. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.output_total_le_darts line 281
  35. theorem OAI.MinUncutGames.Foundations.PCP.RoundSize.output_total_le line 307
  36. theorem OAI.MinUncutGames.Foundations.Hastad.SourceNonempty.real_clause_gap_of_count line 322
  37. theorem OAI.MinUncutGames.Foundations.Hastad.SourceNonempty.clauseGap_of_count line 336
  38. theorem OAI.MinUncutGames.Foundations.Hastad.SourceNonempty.cnf_nonempty_of_nonempty_darts line 347
  39. theorem OAI.MinUncutGames.Foundations.Hastad.SourceNonempty.cnf_clauseGap line 356
  40. theorem OAI.MinUncutGames.Foundations.Hastad.SourceNonempty.cnf_clauseGap_unit line 368
  41. abbrev OAI.MinUncutGames.Foundations.PCP.PCPIteration.Label line 390
  42. abbrev OAI.MinUncutGames.Foundations.PCP.PCPIteration.Graph line 391
  43. abbrev OAI.MinUncutGames.Foundations.PCP.PCPIteration.Addresses line 392
  44. def OAI.MinUncutGames.Foundations.PCP.PCPIteration.step line 394
  45. def OAI.MinUncutGames.Foundations.PCP.PCPIteration.run line 398
  46. def OAI.MinUncutGames.Foundations.PCP.PCPIteration.initial line 401
  47. def OAI.MinUncutGames.Foundations.PCP.PCPIteration.iterationCount line 403
  48. def OAI.MinUncutGames.Foundations.PCP.PCPIteration.output line 405
  49. def OAI.MinUncutGames.Foundations.PCP.PCPIteration.polynomialDegree line 408
  50. def OAI.MinUncutGames.Foundations.PCP.PCPIteration.finalClauseGap line 410
  51. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.finalClauseGap_positive line 412
  52. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.sizeFactor_le_power line 416
  53. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.initial_satisfiable_iff line 419
  54. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.initial_size_positive line 423
  55. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.initial_size_bound line 426
  56. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.step_completeness line 434
  57. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.step_gap line 438
  58. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.step_size line 442
  59. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.run_completeness line 446
  60. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.run_gap line 452
  61. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.run_size line 458
  62. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.output_completeness line 464
  63. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.output_gap line 470
  64. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.output_satisfiable_iff line 480
  65. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.output_size_polynomial line 490
  66. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.output_size_clause_bound line 497
  67. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.output_count_gap line 505
  68. def OAI.MinUncutGames.Foundations.PCP.PCPIteration.finalCNF line 531
  69. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.finalCNF_satisfiable_iff line 534
  70. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.finalCNF_clause_count line 539
  71. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.finalCNF_variable_count line 543
  72. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.finalCNF_nonempty line 547
  73. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.finalCNF_gap line 554
  74. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.finalCNF_clauseGap line 566
  75. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.finalCNF_total_size line 572
  76. theorem OAI.MinUncutGames.Foundations.PCP.PCPIteration.finalCNF_polynomial_size line 589
  77. def OAI.MinUncutGames.Foundations.PCP.FinalTableFormula.output line 608
  78. theorem OAI.MinUncutGames.Foundations.PCP.FinalTableFormula.satisfiable_iff line 611
  79. theorem OAI.MinUncutGames.Foundations.PCP.FinalTableFormula.variable_count line 618
  80. theorem OAI.MinUncutGames.Foundations.PCP.FinalTableFormula.clause_count line 622
  81. theorem OAI.MinUncutGames.Foundations.PCP.FinalTableFormula.nonempty line 626
  82. theorem OAI.MinUncutGames.Foundations.PCP.FinalTableFormula.tableGraph_rejectionCount line 630
  83. theorem OAI.MinUncutGames.Foundations.PCP.FinalTableFormula.tableGraph_count_lower line 640
  84. theorem OAI.MinUncutGames.Foundations.PCP.FinalTableFormula.clauseGap line 649
  85. theorem OAI.MinUncutGames.Foundations.PCP.FinalTableFormula.total_size_le line 659
  86. def OAI.MinUncutGames.Foundations.PCP.FinalTableFormula.sizePolynomial line 666
  87. theorem OAI.MinUncutGames.Foundations.PCP.FinalTableFormula.sizePolynomial_eval line 671
  88. theorem OAI.MinUncutGames.Foundations.PCP.FinalTableFormula.formulaBits_length_le_polynomial line 675