OAI/Probability/SKGap/Localization/BlockDegree.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.Noncrossing.InverseDiagram.blockDegree line 17
2. def OAI.SKGap.Noncrossing.InverseDiagram.blockEnumerate line 19
3. def OAI.SKGap.Noncrossing.InverseDiagram.Blocks line 25
4. lemma OAI.SKGap.Noncrossing.InverseDiagram.blockDegree_nil line 27
5. lemma OAI.SKGap.Noncrossing.InverseDiagram.blockDegree_true line 28
6. lemma OAI.SKGap.Noncrossing.InverseDiagram.blockDegree_false line 30
7. lemma OAI.SKGap.Noncrossing.InverseDiagram.mem_blockEnumerate line 33
8. lemma OAI.SKGap.Noncrossing.InverseDiagram.blockEnumerate_nodup line 63
9. instance OAI.SKGap.Noncrossing.InverseDiagram.blocksFintype line 83
10. def OAI.SKGap.Noncrossing.InverseDiagram.LiteralPaired line 88
11. instance OAI.SKGap.Noncrossing.InverseDiagram.literalPairedFintype line 89
12. def OAI.SKGap.Noncrossing.InverseDiagram.AtDegree line 92
13. instance OAI.SKGap.Noncrossing.InverseDiagram.atDegreeFintype line 93
14. def OAI.SKGap.Noncrossing.InverseDiagram.toLiteral line 98
15. lemma OAI.SKGap.Noncrossing.InverseDiagram.toLiteral_bijective line 103
16. def OAI.SKGap.Noncrossing.InverseDiagram.literalEquiv line 124
17. lemma OAI.SKGap.Noncrossing.InverseDiagram.literal_odd_empty line 127
18. def OAI.SKGap.Noncrossing.InverseDiagram.blockLabel line 139
19. lemma OAI.SKGap.Noncrossing.InverseDiagram.toDiagram_value line 143
20. def OAI.SKGap.Noncrossing.InverseDiagram.literalCoefficient line 166
21. lemma OAI.SKGap.Noncrossing.InverseDiagram.literalCoefficient_even line 169
22. lemma OAI.SKGap.Noncrossing.InverseDiagram.literalCoefficient_odd line 186
23. theorem OAI.SKGap.Noncrossing.InverseDiagram.literalCoefficient_eq line 191