OAI/Combinatorics/KMedian/PCP/AlphabetReduction.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.PCP.BinaryCSP line 14
  2. def OAI.MetricKMedian.PCP.BinaryCSP.Satisfies line 21
  3. def OAI.MetricKMedian.PCP.BinaryCSP.rejection line 22
  4. structure OAI.MetricKMedian.PCP.FourCSP line 26
  5. def OAI.MetricKMedian.PCP.FourCSP.Satisfies line 30
  6. def OAI.MetricKMedian.PCP.FourCSP.rejection line 31
  7. def OAI.MetricKMedian.PCP.FourQuery.map line 36
  8. theorem OAI.MetricKMedian.PCP.FourQuery.map_rejects line 37
  9. theorem OAI.MetricKMedian.PCP.testRate_eq_zero_iff line 41
  10. abbrev OAI.MetricKMedian.PCP.AlphabetReduction.Relations line 50
  11. abbrev OAI.MetricKMedian.PCP.AlphabetReduction.UniversalPad line 51
  12. abbrev OAI.MetricKMedian.PCP.AlphabetReduction.EdgeSample line 52
  13. abbrev OAI.MetricKMedian.PCP.AlphabetReduction.relation line 56
  14. abbrev OAI.MetricKMedian.PCP.AlphabetReduction.Interior line 57
  15. abbrev OAI.MetricKMedian.PCP.AlphabetReduction.Position line 59
  16. abbrev OAI.MetricKMedian.PCP.AlphabetReduction.Test line 60
  17. def OAI.MetricKMedian.PCP.AlphabetReduction.localMap line 62
  18. def OAI.MetricKMedian.PCP.AlphabetReduction.reduced line 67
  19. def OAI.MetricKMedian.PCP.AlphabetReduction.vertexTable line 71
  20. def OAI.MetricKMedian.PCP.AlphabetReduction.firstTable line 73
  21. def OAI.MetricKMedian.PCP.AlphabetReduction.secondTable line 75
  22. theorem OAI.MetricKMedian.PCP.AlphabetReduction.restriction line 80
  23. theorem OAI.MetricKMedian.PCP.AlphabetReduction.edge_rate line 92
  24. def OAI.MetricKMedian.PCP.AlphabetReduction.decoded line 115
  25. theorem OAI.MetricKMedian.PCP.AlphabetReduction.sound line 119
  26. theorem OAI.MetricKMedian.PCP.AlphabetReduction.complete line 143