OAI/Combinatorics/KMedian/Amplification/PoweringObjects.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.reverse_end line 15
  2. def OAI.MetricKMedian.PCP.PortGraph.Walk.centerEquiv line 18
  3. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.center_vertex line 23
  4. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.center_port line 27
  5. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.center_left_end line 31
  6. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.center_right_end line 36
  7. structure OAI.MetricKMedian.PCP.PortCSP line 50
  8. def OAI.MetricKMedian.PCP.PortCSP.Satisfies line 58
  9. def OAI.MetricKMedian.PCP.PortCSP.Bad line 59
  10. instance OAI.MetricKMedian.PCP.PortCSP.badDecidable line 61
  11. theorem OAI.MetricKMedian.PCP.PortCSP.bad_symmetric line 64
  12. abbrev OAI.MetricKMedian.PCP.Advice line 72
  13. def OAI.MetricKMedian.PCP.Advice.get line 78
  14. theorem OAI.MetricKMedian.PCP.Advice.get_le line 81
  15. def OAI.MetricKMedian.PCP.PortGraph.honest line 89
  16. def OAI.MetricKMedian.PCP.PortGraph.opinion line 92
  17. theorem OAI.MetricKMedian.PCP.PortGraph.honest_opinion line 95