OAI/Combinatorics/IndependentSets/Expansion/PoweringTest.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.baseGraph line 12
  2. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.pathAccepts line 21
  3. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.pathAccepts_eq_true_iff line 29
  4. abbrev OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.Dart line 40
  5. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.reverseDart line 42
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.reverseDart_involutive line 52
  7. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.poweredGraph line 57
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.poweredGraph_tail_false line 69
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.poweredGraph_tail_true line 74
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.poweredGraph_edgeSatisfied line 79
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.rejection_mean_eq_path_mean line 88
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.pathAccepts_honest line 99
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.perfect_completeness line 113
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.preserves_satisfiability line 124
  15. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.decodedBad line 136
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.decodedBad_eq_true_iff line 140
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.decodedBad_rot line 146
  18. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.witness line 155
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.witness_bad line 167
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.witness_implies_path_rejection line 175
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTest.witness_implies_rejection line 202