OAI/Analysis/Littlewood/SlotGraph.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AsymptoticallyMinimalLittlewood.Packing.slotVertices line 16
2. def OAI.AsymptoticallyMinimalLittlewood.Packing.slotEdges line 19
3. def OAI.AsymptoticallyMinimalLittlewood.Packing.slotSupport line 22
4. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.mem_slotSupport line 26
5. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.slotSupport_card line 31
6. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.slotSupport_subset line 38
7. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.slotVertices_card line 47
8. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.slot_degree_fiber line 53
9. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.slot_codegree_subset line 72
10. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.slot_same_row_disjoint line 84
11. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.slot_codegree line 93
12. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.prod_indicator_eq line 120
13. def OAI.AsymptoticallyMinimalLittlewood.Packing.slotDensity line 130
14. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.slotDensity_eq line 135
15. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.slot_degree_density line 147
16. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.slot_degree_near line 162
17. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.random_slot_matching line 185
18. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.concrete_slot_variance line 256
19. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.concrete_slot_vertices_card line 287