OAI/Combinatorics/KMedian/Expanders/GraphMix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedian.PCP.l2_scale line 12
2. abbrev OAI.MetricKMedian.PCP.PortGraph.BlendPort line 28
3. def OAI.MetricKMedian.PCP.PortGraph.blendRotate line 30
4. lemma OAI.MetricKMedian.PCP.PortGraph.blendRotate_involutive line 35
5. def OAI.MetricKMedian.PCP.PortGraph.blend line 39
6. lemma OAI.MetricKMedian.PCP.PortGraph.blend_step line 46
7. lemma OAI.MetricKMedian.PCP.PortGraph.blend_adjacency line 53
8. theorem OAI.MetricKMedian.PCP.PortGraph.blend_contracts line 65
9. lemma OAI.MetricKMedian.PCP.PortGraph.contracts_one line 92
10. lemma OAI.MetricKMedian.PCP.PortGraph.blend_half line 96