OAI/Combinatorics/KMedian/Amplification/Majority.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.PortGraph.vote line 17
2. def OAI.MetricKMedian.PCP.PortGraph.mass line 20
3. def OAI.MetricKMedian.PCP.PortGraph.totalMass line 23
4. lemma OAI.MetricKMedian.PCP.PortGraph.vote_nonneg line 27
5. lemma OAI.MetricKMedian.PCP.PortGraph.vote_sum line 29
6. lemma OAI.MetricKMedian.PCP.PortGraph.mass_nonneg line 36
7. lemma OAI.MetricKMedian.PCP.PortGraph.mass_sum line 41
8. lemma OAI.MetricKMedian.PCP.PortGraph.exists_plurality line 49
9. def OAI.MetricKMedian.PCP.PortGraph.plurality line 54
10. lemma OAI.MetricKMedian.PCP.PortGraph.plurality_max line 58
11. lemma OAI.MetricKMedian.PCP.PortGraph.plurality_mass line 62
12. lemma OAI.MetricKMedian.PCP.PortGraph.totalMass_nonneg line 72
13. lemma OAI.MetricKMedian.PCP.PortGraph.totalMass_eq line 75
14. def OAI.MetricKMedian.PCP.PortCSP.rootHit line 87
15. def OAI.MetricKMedian.PCP.PortCSP.cutHit line 94
16. lemma OAI.MetricKMedian.PCP.PortCSP.rootHit_nonneg line 98
17. lemma OAI.MetricKMedian.PCP.PortCSP.rootHit_le line 105
18. theorem OAI.MetricKMedian.PCP.PortCSP.cutHit_mean line 112