OAI/Probability/SwitchChain/FixedBlockPartitions.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem315.FixedBlock.row line 12
2. lemma OAI.Problem315.FixedBlock.mem_row line 16
3. lemma OAI.Problem315.FixedBlock.row_relabel line 21
4. abbrev OAI.Problem315.FixedBlock.Partition line 26
5. def OAI.Problem315.FixedBlock.relabel line 29
6. lemma OAI.Problem315.FixedBlock.relabel_val line 36
7. lemma OAI.Problem315.FixedBlock.relabel_one line 40
8. lemma OAI.Problem315.FixedBlock.relabel_mul line 43
9. lemma OAI.Problem315.FixedBlock.row_swap_unchanged line 49
10. lemma OAI.Problem315.FixedBlock.exists_unused_color line 62
11. lemma OAI.Problem315.FixedBlock.three_sum_sq_le_twice line 65
12. lemma OAI.Problem315.FixedBlock.row_transposition_energy line 79
13. lemma OAI.Problem315.FixedBlock.exists_relabel line 90
14. lemma OAI.Problem315.FixedBlock.eq_of_swap_invariant line 107