OAI/Probability/SKGap/Matrix/InverseDiagram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.SKGap.Noncrossing.InverseDiagram line 12
2. def OAI.SKGap.Noncrossing.InverseDiagram.degree line 20
3. def OAI.SKGap.Noncrossing.InverseDiagram.blocks line 25
4. theorem OAI.SKGap.Noncrossing.InverseDiagram.blocks_degree line 30
5. def OAI.SKGap.Noncrossing.InverseDiagram.enumerate line 39
6. lemma OAI.SKGap.Noncrossing.InverseDiagram.mem_enumerate line 48
7. lemma OAI.SKGap.Noncrossing.InverseDiagram.nodup_arch_list line 78
8. theorem OAI.SKGap.Noncrossing.InverseDiagram.enumerate_nodup line 91
9. def OAI.SKGap.Noncrossing.InverseDiagram.average line 126
10. def OAI.SKGap.Noncrossing.InverseDiagram.value line 128
11. def OAI.SKGap.Noncrossing.InverseDiagram.coefficient line 133
12. lemma OAI.SKGap.Noncrossing.InverseDiagram.coefficient_zero line 136
13. lemma OAI.SKGap.Noncrossing.InverseDiagram.average_add line 139
14. lemma OAI.SKGap.Noncrossing.InverseDiagram.average_zero line 142
15. lemma OAI.SKGap.Noncrossing.InverseDiagram.average_list_sum line 144
16. lemma OAI.SKGap.Noncrossing.InverseDiagram.sum_flatMap line 154
17. lemma OAI.SKGap.Noncrossing.InverseDiagram.sum_arch line 160
18. lemma OAI.SKGap.Noncrossing.InverseDiagram.coefficient_succ line 173
19. theorem OAI.SKGap.Noncrossing.InverseDiagram.coefficient_positive line 189
20. def OAI.SKGap.Noncrossing.InverseDiagram.predictionSeries line 207
21. theorem OAI.SKGap.Noncrossing.InverseDiagram.predictionSeries_eq_one line 210