OAI/Combinatorics/KMedian/Expanders/CloudOrder.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Compiler.CloudOrder.boolOrder line 14
2. def OAI.MetricKMedian.PCP.Compiler.CloudOrder.dartOrder line 15
3. def OAI.MetricKMedian.PCP.Compiler.CloudOrder.activeOrder line 16
4. def OAI.MetricKMedian.PCP.Compiler.CloudOrder.incidentOrder line 19
5. def OAI.MetricKMedian.PCP.Compiler.CloudOrder.copyOrder line 21
6. def OAI.MetricKMedian.PCP.Compiler.CloudOrder.nodeOrder line 23
7. lemma OAI.MetricKMedian.PCP.Compiler.CloudOrder.copy_index_bound line 25
8. def OAI.MetricKMedian.PCP.Compiler.CloudOrder.cloudEmbed line 33
9. lemma OAI.MetricKMedian.PCP.Compiler.CloudOrder.cloudEmbed_index line 36
10. def OAI.MetricKMedian.PCP.Compiler.CloudOrder.nodeCode line 44
11. lemma OAI.MetricKMedian.PCP.Compiler.CloudOrder.sigmaCode_injective line 46
12. lemma OAI.MetricKMedian.PCP.Compiler.CloudOrder.nodeCode_injective line 56
13. lemma OAI.MetricKMedian.PCP.Compiler.CloudOrder.pad_index_bound line 64
14. def OAI.MetricKMedian.PCP.Compiler.CloudOrder.padEmbed line 72
15. lemma OAI.MetricKMedian.PCP.Compiler.CloudOrder.padEmbed_index line 76