OAI/Probability/SwitchChain/DisjointProjectionCell.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.DisjointEncoding.pair_count_eq line 14
2. theorem OAI.Problem315.DisjointEncoding.sameCell_of_sameFiber_left line 22
3. theorem OAI.Problem315.DisjointEncoding.sameCell_of_sameFiber_right line 44
4. def OAI.Problem315.DisjointEncoding.stateCellSetoid line 66
5. abbrev OAI.Problem315.DisjointEncoding.CellIndex line 71
6. instance OAI.Problem315.DisjointEncoding.(instance at line 73) line 73
7. def OAI.Problem315.DisjointEncoding.cellIndex line 75
8. theorem OAI.Problem315.DisjointEncoding.cellIndex_eq_iff line 77
9. theorem OAI.Problem315.DisjointEncoding.cellInvariant_left line 81
10. theorem OAI.Problem315.DisjointEncoding.cellInvariant_right line 88
11. theorem OAI.Problem315.DisjointEncoding.interaction_eq_sum_cells line 95
12. theorem OAI.Problem315.DisjointEncoding.interaction_bound_of_cell_bounds line 106