OAI/Computability/BinPacking/PCP/PreprocessingGuarantees.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.BaseTable line 9
  2. def OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.degree line 11
  3. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.degree_eq line 13
  4. def OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.regularVertices line 18
  5. def OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.vertices line 19
  6. def OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.padded line 21
  7. def OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.overlayFamily line 26
  8. def OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.preprocess line 31
  9. def OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.output line 36
  10. def OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.graphTable line 39
  11. def OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.outputBits line 42
  12. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.regularVertices_ge_darts line 45
  13. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.regularVertices_le line 49
  14. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.vertices_positive line 52
  15. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.vertices_le_of_positive line 55
  16. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.vertices_eq_one_of_no_darts line 65
  17. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.vertices_le line 70
  18. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.darts_eq line 80
  19. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.darts_le line 83
  20. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.vertices_le_inputBits line 91
  21. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingTables.darts_le_inputBits line 96
  22. abbrev OAI.BinPackingGames.Foundations.PCP.PreprocessingStageMaps.BaseTable line 107
  23. def OAI.BinPackingGames.Foundations.PCP.PreprocessingStageMaps.regular line 109
  24. def OAI.BinPackingGames.Foundations.PCP.PreprocessingStageMaps.padding line 112
  25. def OAI.BinPackingGames.Foundations.PCP.PreprocessingStageMaps.familyAt line 116
  26. def OAI.BinPackingGames.Foundations.PCP.PreprocessingStageMaps.paddedOverlay line 121
  27. def OAI.BinPackingGames.Foundations.PCP.PreprocessingStageMaps.lazy line 126
  28. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingStageMaps.output_eq line 129
  29. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingGuarantees.overlay_rejectionCount line 145
  30. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingGuarantees.lazy_rejectionCount line 159
  31. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingGuarantees.overlayFamily_certificate line 173
  32. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingGuarantees.overlay_certificate line 181
  33. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingGuarantees.spectral_certificate line 190
  34. def OAI.BinPackingGames.Foundations.PCP.PreprocessingGuarantees.restrictedLabel line 198
  35. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingGuarantees.rejectionCount_eq_regularized line 203
  36. def OAI.BinPackingGames.Foundations.PCP.PreprocessingGuarantees.roundLabels line 211
  37. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingGuarantees.soundness line 215
  38. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingGuarantees.completeness line 223
  39. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingGuarantees.gap_transfer_real line 236