OAI/Computability/DirectedFeedback/Games/PoweringFinalConstants.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Foundations.PCP.PoweringFinalConstants.Alphabet line 8
  2. theorem OAI.DFVSGames.Foundations.PCP.PoweringFinalConstants.card_alphabet line 10
  3. theorem OAI.DFVSGames.Foundations.PCP.PoweringFinalConstants.card_alphabet_eq_final line 13
  4. theorem OAI.DFVSGames.Foundations.PCP.PoweringFinalConstants.center_eq line 16
  5. theorem OAI.DFVSGames.Foundations.PCP.PoweringFinalConstants.walkLength_eq line 22
  6. theorem OAI.DFVSGames.Foundations.PCP.PoweringFinalConstants.spectral_denominator_eq line 28
  7. theorem OAI.DFVSGames.Foundations.PCP.PoweringFinalConstants.gain_eq line 32
  8. theorem OAI.DFVSGames.Foundations.PCP.PoweringFinalConstants.gain_card_eq line 50
  9. theorem OAI.DFVSGames.Foundations.PCP.PoweringFinalConstants.scaled_bound_eq line 56
  10. theorem OAI.DFVSGames.Foundations.PCP.PoweringFinalConstants.composed_scaled_gap line 66
  11. def OAI.DFVSGames.Foundations.PCP.RoundGap.poweredLower line 86
  12. theorem OAI.DFVSGames.Foundations.PCP.RoundGap.poweredLower_nonnegative line 90
  13. theorem OAI.DFVSGames.Foundations.PCP.RoundGap.powered_count_gap line 98
  14. theorem OAI.DFVSGames.Foundations.PCP.RoundGap.amplifies line 126
  15. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.card_padded_alphabet line 149
  16. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.card_powered_dart line 156
  17. opaque OAI.DFVSGames.Foundations.PCP.RoundSize.lockedNat line 163
  18. def OAI.DFVSGames.Foundations.PCP.RoundSize.poweredAlphabetSize line 165
  19. def OAI.DFVSGames.Foundations.PCP.RoundSize.poweredDartFactor line 169
  20. def OAI.DFVSGames.Foundations.PCP.RoundSize.sizeFactor line 172
  21. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.poweredAlphabetSize_eq line 176
  22. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.poweredDartFactor_eq line 180
  23. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.sizeFactor_eq line 184
  24. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.coefficient_positive_inline_RoundSize line 188
  25. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.poweredAlphabet_card line 193
  26. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.sizeFactor_positive line 202
  27. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.factor_total_inline_RoundSize line 208
  28. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.nat_card_output_vertex_inline_RoundSize line 211
  29. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.nat_card_output_dart_inline_RoundSize line 219
  30. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.nat_card_output_total_le_inline_RoundSize line 226
  31. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.poweredDart_card line 238
  32. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.output_vertex_card line 249
  33. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.output_dart_card line 264
  34. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.output_total_le_darts line 276
  35. theorem OAI.DFVSGames.Foundations.PCP.RoundSize.output_total_le line 302
  36. theorem OAI.DFVSGames.Foundations.Hastad.SourceNonempty.real_clause_gap_of_count line 315
  37. theorem OAI.DFVSGames.Foundations.Hastad.SourceNonempty.clauseGap_of_count line 329
  38. theorem OAI.DFVSGames.Foundations.Hastad.SourceNonempty.cnf_nonempty_of_nonempty_darts line 340
  39. theorem OAI.DFVSGames.Foundations.Hastad.SourceNonempty.cnf_clauseGap line 349
  40. theorem OAI.DFVSGames.Foundations.Hastad.SourceNonempty.cnf_clauseGap_unit line 361
  41. abbrev OAI.DFVSGames.Foundations.PCP.PCPIteration.Label line 381
  42. abbrev OAI.DFVSGames.Foundations.PCP.PCPIteration.Graph line 382
  43. abbrev OAI.DFVSGames.Foundations.PCP.PCPIteration.Addresses line 383
  44. def OAI.DFVSGames.Foundations.PCP.PCPIteration.step line 385
  45. def OAI.DFVSGames.Foundations.PCP.PCPIteration.run line 389
  46. def OAI.DFVSGames.Foundations.PCP.PCPIteration.initial line 392
  47. def OAI.DFVSGames.Foundations.PCP.PCPIteration.iterationCount line 394
  48. def OAI.DFVSGames.Foundations.PCP.PCPIteration.output line 396
  49. def OAI.DFVSGames.Foundations.PCP.PCPIteration.polynomialDegree line 399
  50. def OAI.DFVSGames.Foundations.PCP.PCPIteration.finalClauseGap line 401
  51. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.finalClauseGap_positive line 403
  52. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.sizeFactor_le_power line 407
  53. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.initial_satisfiable_iff line 410
  54. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.initial_size_positive line 414
  55. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.initial_size_bound line 417
  56. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.step_completeness line 425
  57. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.step_gap line 429
  58. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.step_size line 433
  59. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.run_completeness line 437
  60. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.run_gap line 443
  61. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.run_size line 449
  62. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.output_completeness line 455
  63. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.output_gap line 461
  64. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.output_satisfiable_iff line 471
  65. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.output_size_polynomial line 481
  66. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.output_size_clause_bound line 488
  67. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.output_count_gap line 496
  68. def OAI.DFVSGames.Foundations.PCP.PCPIteration.finalCNF line 520
  69. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.finalCNF_satisfiable_iff line 523
  70. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.finalCNF_clause_count line 528
  71. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.finalCNF_variable_count line 532
  72. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.finalCNF_nonempty line 536
  73. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.finalCNF_gap line 543
  74. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.finalCNF_clauseGap line 555
  75. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.finalCNF_total_size line 561
  76. theorem OAI.DFVSGames.Foundations.PCP.PCPIteration.finalCNF_polynomial_size line 578
  77. def OAI.DFVSGames.Foundations.PCP.FinalTableFormula.output line 594
  78. theorem OAI.DFVSGames.Foundations.PCP.FinalTableFormula.satisfiable_iff line 597
  79. theorem OAI.DFVSGames.Foundations.PCP.FinalTableFormula.variable_count line 604
  80. theorem OAI.DFVSGames.Foundations.PCP.FinalTableFormula.clause_count line 608
  81. theorem OAI.DFVSGames.Foundations.PCP.FinalTableFormula.nonempty line 612
  82. theorem OAI.DFVSGames.Foundations.PCP.FinalTableFormula.tableGraph_rejectionCount line 616
  83. theorem OAI.DFVSGames.Foundations.PCP.FinalTableFormula.tableGraph_count_lower line 626
  84. theorem OAI.DFVSGames.Foundations.PCP.FinalTableFormula.clauseGap line 635
  85. theorem OAI.DFVSGames.Foundations.PCP.FinalTableFormula.total_size_le line 645
  86. def OAI.DFVSGames.Foundations.PCP.FinalTableFormula.sizePolynomial line 652
  87. theorem OAI.DFVSGames.Foundations.PCP.FinalTableFormula.sizePolynomial_eval line 657
  88. theorem OAI.DFVSGames.Foundations.PCP.FinalTableFormula.formulaBits_length_le_polynomial line 661
  89. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineBudget.nameSum line 683
  90. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineBudget.bodyTime line 686
  91. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineBudget.loopTime line 690
  92. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineBudget.nameSum_le line 694
  93. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineBudget.bodyTime_le line 701
  94. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineBudget.loopTime_le line 708
  95. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineBudget.input_header_bound line 730
  96. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineBudget.graph_size_bound line 736
  97. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineBudget.fullBudget line 743
  98. def OAI.DFVSGames.Foundations.PCP.RawInitialMachineBudget.timePolynomial line 747
  99. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineBudget.timePolynomial_eval line 751
  100. theorem OAI.DFVSGames.Foundations.PCP.RawInitialMachineBudget.fullBudget_le line 755