OAI/Probability/SignedSweeps/PairDecomposition.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.starProjection_trace line 15
2. lemma OAI.SignedSweeps.wordTypeProjection_trace line 23
3. lemma OAI.SignedSweeps.pairTypeProjection_trace line 28
4. lemma OAI.SignedSweeps.pairTypeProjection_finrank_le line 43
5. lemma OAI.SignedSweeps.pairTypeProjection_zero_of_height line 68
6. abbrev OAI.SignedSweeps.PairType line 79
7. def OAI.SignedSweeps.PairType.projector line 93
8. def OAI.SignedSweeps.PairType.entropy line 97
9. def OAI.SignedSweeps.PairType.height line 99
10. lemma OAI.SignedSweeps.sum_pairTypeProjection_fixed line 113
11. lemma OAI.SignedSweeps.pairAllocationProjection_apply line 129
12. theorem OAI.SignedSweeps.pairTypeProjection_sum line 150