OAI/Combinatorics/KMedian/Amplification/RegularizationObjects.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.PCP.CloudCopies.dartFlip line 18
  2. def OAI.MetricKMedian.PCP.CloudCopies.dartGraph line 24
  3. def OAI.MetricKMedian.PCP.CloudCopies.dartCSP line 28
  4. def OAI.MetricKMedian.PCP.CloudCopies.matchingGraph line 35
  5. def OAI.MetricKMedian.PCP.CloudCopies.matchingCSP line 36
  6. lemma OAI.MetricKMedian.PCP.CloudCopies.matching_bad line 38
  7. def OAI.MetricKMedian.PCP.CloudCopies.equalityCSP line 45
  8. lemma OAI.MetricKMedian.PCP.CloudCopies.equality_bad line 49
  9. abbrev OAI.MetricKMedian.PCP.CloudCopies.RegularPort line 55
  10. def OAI.MetricKMedian.PCP.CloudCopies.regularGraph line 56
  11. def OAI.MetricKMedian.PCP.CloudCopies.regularCSP line 57
  12. def OAI.MetricKMedian.PCP.CloudCopies.honest line 59
  13. lemma OAI.MetricKMedian.PCP.CloudCopies.honest_dart line 62
  14. lemma OAI.MetricKMedian.PCP.CloudCopies.equality_complete line 65
  15. lemma OAI.MetricKMedian.PCP.CloudCopies.matching_complete line 69
  16. lemma OAI.MetricKMedian.PCP.CloudCopies.regular_complete line 84