OAI/Combinatorics/KMedian/Amplification/AmplifierSize.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.PCP.Amplifier.WalkData line 14
2. def OAI.MetricKMedian.PCP.Amplifier.walkCoeff line 15
3. def OAI.MetricKMedian.PCP.Amplifier.nodeCoeff line 16
4. lemma OAI.MetricKMedian.PCP.Amplifier.powered_edge_card line 24
5. lemma OAI.MetricKMedian.PCP.Amplifier.node_card_bound line 34
6. lemma OAI.MetricKMedian.PCP.Amplifier.edge_card_formula line 37
7. lemma OAI.MetricKMedian.PCP.Amplifier.arith_edge_bound line 41
8. lemma OAI.MetricKMedian.PCP.Amplifier.arith_edge_chain line 45
9. lemma OAI.MetricKMedian.PCP.Amplifier.edge_card_bound line 50
10. lemma OAI.MetricKMedian.PCP.Amplifier.node_size_card line 56
11. lemma OAI.MetricKMedian.PCP.Amplifier.arith_size_chain2 line 59
12. lemma OAI.MetricKMedian.PCP.Amplifier.size_bound line 70
13. instance OAI.MetricKMedian.PCP.Amplifier.newEdgeNonempty line 78