OAI/Combinatorics/KMedian/Projection/Tables.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedian.PCP.Compiler.Ordered.entries_ofFn line 18
2. lemma OAI.MetricKMedian.PCP.Compiler.Ordered.map_entries line 25
3. abbrev OAI.MetricKMedian.PCP.Compiler.ProjectionRow line 30
4. abbrev OAI.MetricKMedian.PCP.Compiler.ProjectionTable line 31
5. def OAI.MetricKMedian.PCP.Compiler.ProjectionTable.build line 36
6. def OAI.MetricKMedian.PCP.Compiler.ProjectionTable.raw line 40
7. lemma OAI.MetricKMedian.PCP.Compiler.ProjectionTable.poly_raw line 44
8. def OAI.MetricKMedian.PCP.Compiler.ProjectionTable.indexed line 53
9. lemma OAI.MetricKMedian.PCP.Compiler.ProjectionTable.nu_pos line 56
10. lemma OAI.MetricKMedian.PCP.Compiler.ProjectionTable.order_pos line 61
11. def OAI.MetricKMedian.PCP.Compiler.ProjectionTable.input line 64
12. lemma OAI.MetricKMedian.PCP.Compiler.ProjectionTable.input_raw line 68
13. lemma OAI.MetricKMedian.PCP.Compiler.ProjectionTable.input_perfect line 75
14. lemma OAI.MetricKMedian.PCP.Compiler.ProjectionTable.input_sound line 79