OAI/Combinatorics/KMedian/Amplification/FlexibleAmplifier.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.PCP.FlexibleAmplifier.Node line 21
2. abbrev OAI.MetricKMedian.PCP.FlexibleAmplifier.Edge line 22
3. instance OAI.MetricKMedian.PCP.FlexibleAmplifier.nodeFintype line 23
4. instance OAI.MetricKMedian.PCP.FlexibleAmplifier.edgeFintype line 24
5. def OAI.MetricKMedian.PCP.FlexibleAmplifier.powered line 25
6. def OAI.MetricKMedian.PCP.FlexibleAmplifier.bits line 26
7. abbrev OAI.MetricKMedian.PCP.FlexibleAmplifier.NewNode line 28
8. abbrev OAI.MetricKMedian.PCP.FlexibleAmplifier.NewEdge line 29
9. instance OAI.MetricKMedian.PCP.FlexibleAmplifier.newNodeFintype line 30
10. instance OAI.MetricKMedian.PCP.FlexibleAmplifier.newEdgeFintype line 31
11. def OAI.MetricKMedian.PCP.FlexibleAmplifier.result line 32
12. def OAI.MetricKMedian.PCP.FlexibleAmplifier.poweredAssignment line 34
13. def OAI.MetricKMedian.PCP.FlexibleAmplifier.decoded line 37
14. theorem OAI.MetricKMedian.PCP.FlexibleAmplifier.complete line 41
15. theorem OAI.MetricKMedian.PCP.FlexibleAmplifier.sound line 46