OAI/Combinatorics/KMedian/PCP/Queries.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.PCP.FourQuery line 12
  2. def OAI.MetricKMedian.PCP.FourQuery.Rejects line 18
  3. theorem OAI.MetricKMedian.PCP.testRate_pi_eval line 21
  4. abbrev OAI.MetricKMedian.PCP.LocalRelation.LocalPosition line 35
  5. def OAI.MetricKMedian.PCP.LocalRelation.firstPos line 38
  6. def OAI.MetricKMedian.PCP.LocalRelation.secondPos line 39
  7. def OAI.MetricKMedian.PCP.LocalRelation.leftPos line 40
  8. def OAI.MetricKMedian.PCP.LocalRelation.rightPos line 41
  9. def OAI.MetricKMedian.PCP.LocalRelation.assignment line 43
  10. abbrev OAI.MetricKMedian.PCP.LocalRelation.Sample line 50
  11. instance OAI.MetricKMedian.PCP.LocalRelation.sampleFintype line 58
  12. instance OAI.MetricKMedian.PCP.LocalRelation.sampleNonempty line 66
  13. def OAI.MetricKMedian.PCP.LocalRelation.query line 69
  14. abbrev OAI.MetricKMedian.PCP.LocalRelation.Pad line 87
  15. def OAI.MetricKMedian.PCP.LocalRelation.packed line 89
  16. theorem OAI.MetricKMedian.PCP.LocalRelation.packed_rate line 91
  17. theorem OAI.MetricKMedian.PCP.LocalRelation.packed_sound line 139