OAI/Probability/SwitchChain/TripleMatrixEncoding.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem315.TripleInternalEncoding.rowOffset line 9
2. theorem OAI.Problem315.TripleInternalEncoding.degree_eq_extra_add_offset line 11
3. structure OAI.Problem315.TripleInternalEncoding.TripleCell line 27
4. structure OAI.Problem315.TripleInternalEncoding.AugmentedMatrix line 36
5. def OAI.Problem315.TripleInternalEncoding.encodeCell line 44
6. def OAI.Problem315.TripleInternalEncoding.internalOfAugmented line 63
7. theorem OAI.Problem315.TripleInternalEncoding.extraColumn_internalOfAugmented line 69
8. def OAI.Problem315.TripleInternalEncoding.decodeMatrix line 75
9. theorem OAI.Problem315.TripleInternalEncoding.decode_encode line 92
10. theorem OAI.Problem315.TripleInternalEncoding.encode_decode line 102
11. def OAI.Problem315.TripleInternalEncoding.tripleMatrixEquiv line 111
12. theorem OAI.Problem315.TripleInternalEncoding.rowOffset_le_of_nonempty line 119
13. theorem OAI.Problem315.TripleInternalEncoding.extraColumn_eq_margin_sub_row line 127
14. theorem OAI.Problem315.TripleInternalEncoding.encode_row_eq_iff line 134