OAI/Combinatorics/KMedian/PCP/GlobalRegularization.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.GlobalRegularization.depth line 18
2. abbrev OAI.MetricKMedian.PCP.GlobalRegularization.Node line 19
3. abbrev OAI.MetricKMedian.PCP.GlobalRegularization.FastPort line 20
4. abbrev OAI.MetricKMedian.PCP.GlobalRegularization.StrongPort line 21
5. abbrev OAI.MetricKMedian.PCP.GlobalRegularization.Degree line 22
6. lemma OAI.MetricKMedian.PCP.GlobalRegularization.node_lower line 25
7. lemma OAI.MetricKMedian.PCP.GlobalRegularization.node_relative_upper line 32
8. lemma OAI.MetricKMedian.PCP.GlobalRegularization.node_upper line 40
9. def OAI.MetricKMedian.PCP.GlobalRegularization.embed line 47
10. def OAI.MetricKMedian.PCP.GlobalRegularization.strong line 51
11. lemma OAI.MetricKMedian.PCP.GlobalRegularization.strong_contracts line 55
12. def OAI.MetricKMedian.PCP.GlobalRegularization.padded line 61
13. def OAI.MetricKMedian.PCP.GlobalRegularization.graph line 63
14. def OAI.MetricKMedian.PCP.GlobalRegularization.csp line 65
15. theorem OAI.MetricKMedian.PCP.GlobalRegularization.contracts line 69
16. def OAI.MetricKMedian.PCP.GlobalRegularization.decoded line 72
17. theorem OAI.MetricKMedian.PCP.GlobalRegularization.complete line 75
18. theorem OAI.MetricKMedian.PCP.GlobalRegularization.sound line 80