OAI/Combinatorics/KMedian/Expanders/EqualityExpansion.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedian.PCP.PortGraph.correlation_half line 16
2. def OAI.MetricKMedian.PCP.PortGraph.labelMass line 33
3. def OAI.MetricKMedian.PCP.PortGraph.equalityFailure line 34
4. lemma OAI.MetricKMedian.PCP.PortGraph.labelMass_sum line 37
5. lemma OAI.MetricKMedian.PCP.PortGraph.labelMass_nonneg line 44
6. def OAI.MetricKMedian.PCP.PortGraph.majorityLabel line 46
7. lemma OAI.MetricKMedian.PCP.PortGraph.majorityLabel_max line 52
8. lemma OAI.MetricKMedian.PCP.PortGraph.label_collision_le_majority line 57
9. lemma OAI.MetricKMedian.PCP.PortGraph.label_pairing_sum line 65
10. theorem OAI.MetricKMedian.PCP.PortGraph.equality_cloud_sound line 91