OAI/Combinatorics/IndependentSets/Expansion/PreprocessingTables.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.BaseTable line 13
  2. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.degree line 15
  3. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.degree_eq line 17
  4. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.regularVertices line 22
  5. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.vertices line 23
  6. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.padded line 25
  7. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.overlayFamily line 30
  8. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.preprocess line 35
  9. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.output line 40
  10. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.graphTable line 43
  11. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.outputBits line 46
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.regularVertices_ge_darts line 49
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.regularVertices_le line 53
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.vertices_positive line 56
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.vertices_le_of_positive line 59
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.vertices_eq_one_of_no_darts line 69
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.vertices_le line 74
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.darts_eq line 84
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.darts_le line 87
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.vertices_le_inputBits line 95
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingTables.darts_le_inputBits line 100
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularSoundness.internalDegree_ge_eight line 111
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularSoundness.baseDegree_ne_zero line 115
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularSoundness.resizeTable_certificate line 121
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularSoundness.familyCloudTable_certificate_of_pos line 128
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularSoundness.cloudGraphs_certificate_of_pos line 139
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularSoundness.cloud_expansion line 148
  28. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularSoundness.roundLabels line 170
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularSoundness.soundness line 177
  30. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularSoundness.exists_rounding line 188
  31. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularSoundness.lift_rejectionCount line 197
  32. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularSoundness.completeness line 203
  33. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularSoundness.soundness_of_uniform_lower_bound line 225
  34. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularSoundness.soundness_of_uniform_real_lower_bound line 234