OAI/Combinatorics/IndependentSets/Reduction/OccurrenceTuple.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LargeIndependentSets.occurrenceTuple line 11
2. def OAI.LargeIndependentSets.occurrenceQuestion line 17
3. def OAI.LargeIndependentSets.chainComposite line 21
4. lemma OAI.LargeIndependentSets.chainComposite_self line 32
5. lemma OAI.LargeIndependentSets.chainComposite_comp line 39
6. lemma OAI.LargeIndependentSets.chainComposite_adjacent line 56
7. lemma OAI.LargeIndependentSets.occurrence_chain_imposed line 71
8. lemma OAI.LargeIndependentSets.imposed_path_zero line 85
9. theorem OAI.LargeIndependentSets.occurrence_chain_path_zero line 94
10. def OAI.LargeIndependentSets.paddedList line 131
11. lemma OAI.LargeIndependentSets.mem_paddedList line 134
12. def OAI.LargeIndependentSets.LabelCoverData.Sound line 141
13. theorem OAI.LargeIndependentSets.bounded_list_decoding line 147
14. theorem OAI.LargeIndependentSets.bounded_list_probability line 181