OAI/Combinatorics/KMedian/Expanders/GraphProducts.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.PCP.PortGraph.squareRotate line 15
  2. lemma OAI.MetricKMedian.PCP.PortGraph.squareRotate_involutive line 19
  3. def OAI.MetricKMedian.PCP.PortGraph.square line 23
  4. lemma OAI.MetricKMedian.PCP.PortGraph.square_step line 30
  5. lemma OAI.MetricKMedian.PCP.PortGraph.square_adjacency line 36
  6. theorem OAI.MetricKMedian.PCP.PortGraph.square_contracts line 44
  7. def OAI.MetricKMedian.PCP.PortGraph.zigzagRotate line 51
  8. lemma OAI.MetricKMedian.PCP.PortGraph.zigzagRotate_involutive line 59
  9. def OAI.MetricKMedian.PCP.PortGraph.zigzag line 64
  10. lemma OAI.MetricKMedian.PCP.PortGraph.zigzag_step line 71
  11. def OAI.MetricKMedian.PCP.PortGraph.cloud line 77
  12. def OAI.MetricKMedian.PCP.PortGraph.permute line 79
  13. lemma OAI.MetricKMedian.PCP.PortGraph.zigzag_adjacency line 83