OAI/Combinatorics/KMedian/Expanders/ExpanderFamily.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.PCP.ExpanderFamily.SmallPort line 16
2. abbrev OAI.MetricKMedian.PCP.ExpanderFamily.Degree line 17
3. abbrev OAI.MetricKMedian.PCP.ExpanderFamily.Branch line 18
4. def OAI.MetricKMedian.PCP.ExpanderFamily.growth line 20
5. lemma OAI.MetricKMedian.PCP.ExpanderFamily.growth_gt_one line 22
6. def OAI.MetricKMedian.PCP.ExpanderFamily.baseVertexEquiv line 24
7. def OAI.MetricKMedian.PCP.ExpanderFamily.base line 29
8. lemma OAI.MetricKMedian.PCP.ExpanderFamily.base_contracts line 32
9. def OAI.MetricKMedian.PCP.ExpanderFamily.Vertex line 35
10. instance OAI.MetricKMedian.PCP.ExpanderFamily.vertexFintype line 39
11. instance OAI.MetricKMedian.PCP.ExpanderFamily.vertexNonempty line 43
12. def OAI.MetricKMedian.PCP.ExpanderFamily.graph line 47
13. lemma OAI.MetricKMedian.PCP.ExpanderFamily.graph_contracts line 52
14. lemma OAI.MetricKMedian.PCP.ExpanderFamily.card_branch line 68
15. lemma OAI.MetricKMedian.PCP.ExpanderFamily.card_vertex line 72
16. def OAI.MetricKMedian.PCP.ExpanderFamily.level line 79
17. lemma OAI.MetricKMedian.PCP.ExpanderFamily.padding_lower line 81
18. lemma OAI.MetricKMedian.PCP.ExpanderFamily.padding_upper line 85
19. lemma OAI.MetricKMedian.PCP.ExpanderFamily.recursive_calls_le_size line 90
20. lemma OAI.MetricKMedian.PCP.ExpanderFamily.padded_recursive_calls line 94