OAI/Combinatorics/KMedian/Expanders/ExpanderGuard.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.PCP.Compiler.Expander.State line 11
2. def OAI.MetricKMedian.PCP.Compiler.Expander.guarded line 12
3. lemma OAI.MetricKMedian.PCP.Compiler.Expander.poly_guarded line 14
4. lemma OAI.MetricKMedian.PCP.Compiler.Expander.level_le line 21
5. def OAI.MetricKMedian.PCP.Compiler.Expander.family line 26
6. lemma OAI.MetricKMedian.PCP.Compiler.Expander.family_zero line 27
7. lemma OAI.MetricKMedian.PCP.Compiler.Expander.next_family line 28
8. lemma OAI.MetricKMedian.PCP.Compiler.Expander.family_length line 29
9. lemma OAI.MetricKMedian.PCP.Compiler.Expander.family_wellFormed line 31
10. lemma OAI.MetricKMedian.PCP.Compiler.Expander.guard_at line 34
11. def OAI.MetricKMedian.PCP.Compiler.Expander.sequence line 37
12. lemma OAI.MetricKMedian.PCP.Compiler.Expander.sequence_zero line 39
13. lemma OAI.MetricKMedian.PCP.Compiler.Expander.sequence_succ line 41
14. lemma OAI.MetricKMedian.PCP.Compiler.Expander.iterate_guarded line 52
15. lemma OAI.MetricKMedian.PCP.Compiler.Expander.sequence_wellFormed line 55
16. lemma OAI.MetricKMedian.PCP.Compiler.Expander.sequence_length line 58
17. def OAI.MetricKMedian.PCP.Compiler.Expander.generate line 63
18. lemma OAI.MetricKMedian.PCP.Compiler.Expander.generate_table line 64