OAI/Computability/MaxCut/PCP/Hastad.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaxCutGames.Outer.HastadSource.success line 16
  2. def OAI.MaxCutGames.Outer.HastadSource.asSource line 20
  3. theorem OAI.MaxCutGames.Outer.HastadSource.failure_add_success line 23
  4. def OAI.MaxCutGames.Outer.HastadSource.gapInput line 31
  5. def OAI.MaxCutGames.Outer.HastadSource.sourceMap line 35
  6. def OAI.MaxCutGames.Outer.HastadSource.output line 39
  7. theorem OAI.MaxCutGames.Outer.HastadSource.complete line 43
  8. theorem OAI.MaxCutGames.Outer.HastadSource.sound line 50
  9. def OAI.MaxCutGames.Outer.HastadSource.roundMachine line 59
  10. theorem OAI.MaxCutGames.Outer.HastadSource.roundMachine_finite line 62
  11. def OAI.MaxCutGames.Outer.HastadSource.gapMachine line 67
  12. def OAI.MaxCutGames.Outer.HastadSource.sourceMachine line 75
  13. def OAI.MaxCutGames.Outer.HastadSource.computation line 81
  14. theorem OAI.MaxCutGames.Outer.HastadSource.finiteAlphabet line 86
  15. structure OAI.MaxCutGames.Outer.HastadSource.Reduction line 93
  16. theorem OAI.MaxCutGames.Outer.HastadSource.exists_reduction line 100