OAI/Combinatorics/KMedian/Expanders/ExpanderStep.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.PCP.Compiler.Expander.Raw line 13
2. def OAI.MetricKMedian.PCP.Compiler.Expander.nodeIndex line 14
3. def OAI.MetricKMedian.PCP.Compiler.Expander.rotate line 15
4. def OAI.MetricKMedian.PCP.Compiler.Expander.next line 21
5. lemma OAI.MetricKMedian.PCP.Compiler.Expander.poly_baseRotate line 24
6. lemma OAI.MetricKMedian.PCP.Compiler.Expander.poly_nodeIndex line 25
7. lemma OAI.MetricKMedian.PCP.Compiler.Expander.poly_rotate line 31
8. lemma OAI.MetricKMedian.PCP.Compiler.Expander.poly_rotate4 line 35
9. lemma OAI.MetricKMedian.PCP.Compiler.Expander.poly_next line 40
10. lemma OAI.MetricKMedian.PCP.Compiler.Expander.next_length line 49
11. lemma OAI.MetricKMedian.PCP.Compiler.Expander.lookup_next line 52
12. lemma OAI.MetricKMedian.PCP.Compiler.Expander.rotate_table_aux line 57
13. lemma OAI.MetricKMedian.PCP.Compiler.Expander.graph_rotate_succ line 66
14. lemma OAI.MetricKMedian.PCP.Compiler.Expander.rotate_table line 73