OAI/Combinatorics/KMedian/Expanders/PortWalk.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.PCP.PortGraph line 11
  2. def OAI.MetricKMedian.PCP.PortGraph.step line 17
  3. def OAI.MetricKMedian.PCP.PortGraph.back line 18
  4. theorem OAI.MetricKMedian.PCP.PortGraph.rotate_step_back line 20
  5. theorem OAI.MetricKMedian.PCP.PortGraph.step_back line 22
  6. theorem OAI.MetricKMedian.PCP.PortGraph.back_back line 24
  7. def OAI.MetricKMedian.PCP.PortGraph.trace line 27
  8. theorem OAI.MetricKMedian.PCP.PortGraph.trace_zero line 31
  9. theorem OAI.MetricKMedian.PCP.PortGraph.trace_succ line 34
  10. theorem OAI.MetricKMedian.PCP.PortGraph.trace_chain line 37
  11. structure OAI.MetricKMedian.PCP.PortGraph.Walk line 48
  12. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.ext line 55
  13. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.vertex_eq_trace line 58
  14. def OAI.MetricKMedian.PCP.PortGraph.Walk.ofWord line 66
  15. def OAI.MetricKMedian.PCP.PortGraph.Walk.wordEquiv line 69
  16. instance OAI.MetricKMedian.PCP.PortGraph.Walk.(instance at line 78) line 78
  17. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.card line 80
  18. def OAI.MetricKMedian.PCP.PortGraph.Walk.reverse line 85
  19. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.reverse_reverse line 94
  20. def OAI.MetricKMedian.PCP.PortGraph.Walk.reverseEquiv line 103
  21. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.reverse_start line 106
  22. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.reverse_expect line 109